Definition attempt_lemma {x} (f g : attempt x) (T : (∏ y (pyx : y ≤ x), f y pyx = g y pyx) -> Type) : (∏ (e : attempt_fun f = attempt_fun g), T (λ y pyx, eqtohomot (eqtohomot e y) pyx)) -> ∏ e, T e. Proof. intros HT e. simple refine (transportf _ _ (HT _)). { apply funextsec; intros y; apply funextsec; intros pyx. eapply pathscomp0. { refine (eqtohomot _ _). apply maponpaths. refine (eqtohomot _ _). apply toforallpaths_funextsec. } refine (eqtohomot _ _). apply toforallpaths_funextsec. } Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Univalence.