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.
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
