blob: 37e0cb711932a67bd104012d860dca12afd12663 (
plain)
1
2
3
4
5
6
7
8
9
10
|
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)).
Abort.
|
