blob: 4a1afabe89bb5d3619e09b8d6b39e16a41f1a304 (
plain)
1
2
3
4
5
6
7
|
(* Using tactic "change" under binders *)
Definition add2 n := n +2.
Goal (fun n => n) = (fun n => n+2).
change (?n + 2) with (add2 n).
match goal with |- _ = (fun n => add2 n) => idtac end. (* To test the presence of add2 *)
Abort.
|
