Inductive SFalse : SProp := . Definition adjust_of_sprop {A} {x y : A} (pf : x <> y) : x <> y
:= fun e : x = y => SFalse_ind (fun _ => False) (match pf e withend).
Definition adjust_of_sprop_idempotent {A x y pf} : @adjust_of_sprop A x y (@adjust_of_sprop A x y pf) = @adjust_of_sprop A x y pf. Proof. cbv [adjust_of_sprop]; reflexivity. Defined. Definition adjust_of_sprop_idempotent' {A x y pf} : @adjust_of_sprop A x y (@adjust_of_sprop A x y pf) = @adjust_of_sprop A x y pf
:= Eval cbv in @adjust_of_sprop_idempotent A x y pf.
Inductive sF : SProp := .
Definition ff (x y:sF) : match x return nat withend = match y withend := eq_refl.
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.
