Goal False. Proof. set (H1:=I). set (x:=true). assert (H2: x = true) byreflexivity. set (y:=false). assert (H3: y = false) byreflexivity.
clearbody H1 x y.
eenough (H4: _ = false).
vm_compute in H4. (* H4 now has "x:=y" in the evar context. *)
2: exact H3. matchtype of H4 with y = false => idtacend. 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.
