Lemma bar : foo Type. Proof. change foo with (fun x : Type => foo x). (* We shouldn't lose the constraint here *)
cbv beta. elim admit. Defined. (* Illegal application error *)
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.
