blob: a66ee6b3fa29e90d5d11c0ab25e5273f618b1097 (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
Lemma test_bug : forall (R:nat->nat->Prop) n m m' (P: Prop),
P ->
(P -> R n m) ->
(P -> R n m') ->
(forall u, R n u -> u = u -> True) ->
True.
Proof.
intros * HP H1 H2 H3. eapply H3.
eauto. (* H1 is used, but H2 should be used since it is the last hypothesis *)
auto.
Qed.
|
