blob: 7e3c78dc2e8a74d4bfb3389235e51ab929b251e5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
Ltac induction_last :=
let v := match goal with
| |- forall x y, _ = _ -> _ => 1
| |- forall x y, _ -> _ = _ -> _ => 2
| |- forall x y, _ -> _ -> _ = _ -> _ => 3
end in
induction v.
Goal forall n m : nat, True -> n = m -> m = n.
induction_last.
reflexivity.
Qed.
|
