aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/opened/3100.v
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)).