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.
|
