(* Regression wrt v8.4 related to the change of order of resolution of evar-evar unification problems. *) Goalexists x, x=1 -> True.
eexists. intro H. poseproof (f_equal (fun k => k) H).
Undo. pose (@f_equal _ _ S _ _ H). Abort.
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.
