(* Check that an anomaly is not raised *) Goalexists x, x. Proof. simple refine (ex_intro _ _ _).
shelve. (* The failure is due to Type(u)<=Prop for u an arbitrary sort
variable being rejected *) simple refine (_ _). 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.
