blob: 7d153d9828c477e44bb1742e1a35ab2234cc20ec (
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.
|
