blob: 6f35a74dc19a46af4f016c4af545d1a7dfff22f0 (
plain)
1
2
3
4
5
6
7
8
9
|
Fixpoint F (n : nat) (A : Type) : Type :=
match n with
| 0 => True
| S n => forall (x : A), F n (x = x)
end.
Goal forall A n, (forall (x : A) (e : x = x), F n (e = e)).
intros A n.
Fail change (forall x, F n (x = x)) with (F (S n)).
|
