Set Printing Existential Instances. Set Printing All. Goallet y:=0 in exists x:y=y, x = x. intros.
eexists.
rename y into z. unfold z at 1 2. (* should fail because the evar type depends on z *)
Fail clear z. 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.
