|
Definition proj1_sig_path {A} {P : A -> Prop} {u v : sig P} (p : u = v)
: proj1_sig u = proj1_sig v
:= f_equal (@proj1_sig _ _) p.
Definition proj2_sig_path {A} {P : A -> Prop} {u v : sig P} (p : u = v)
: eq_rect _ _ (proj2_sig u) _ (proj1_sig_path p) = proj2_sig v
:= match p with eq_refl => eq_refl end.
Goal forall sz : nat,
let sz' := sz in
forall pf : sz = sz',
let feq_refl := exist (fun x : nat => sz = x) sz' eq_refl in
let fpf := exist (fun x : nat => sz = x) sz' pf in feq_refl = fpf ->
proj2_sig feq_refl = proj2_sig fpf.
Proof.
intros.
etransitivity; [ | exact (proj2_sig_path H) ].
Fail clearbody fpf.
Abort.
¤ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
|
