Definition f := fun X (A : X -> Type) (P : forall x, A x -> Type) x y =>
existT (fun f => forall x, P x (f x)) x y : sigT (fun f => forall x, P x (f x)).
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.
