aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/2375.v
blob: c17c426cdab4e58963276262a4eeaee1642e794c (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
(* In the following code, the (superfluous) lemma [lem] is responsible 
for the failure of congruence. *)

Definition  f : nat -> Prop := fun x => True.

Lemma lem : forall x,  (True -> True)   = ( True ->  f x).
Proof.
  intros. reflexivity.
Qed.

Goal forall  (x:nat), x = x.
Proof.
  intros.
  assert (lem := lem).
  (*clear ax.*)
  congruence.
Qed.