Definition attempt_paths {x} (f g : attempt x) : ∏ (e_fun : ∏ y pyx, f y pyx = g y pyx), (∏ y pyx, attempt_comp f y pyx @ maponpaths (H y) (funextsec (λ z, funextsec (λ lzy, e_fun z (cons (idpath z) lzy pyx)))) = e_fun y pyx @ attempt_comp g y pyx) -> f = g. Proof. use attempt_lemma. intros e. induction f as [f0 f1], g as [g0 g1]. cbn in e. induction e. cbn. intros e_comp. apply maponpaths. apply funextsec; intros y; apply funextsec; intros pyx. refine (!_ @ e_comp _ _). refine (maponpaths _ _ @ pathscomp0rid _). refine (@maponpaths _ _ _ _ (idpath _) _). refine (maponpaths funextsec _ @ funextsec_toforallpaths _). apply funextsec; intros z. apply (funextsec_toforallpaths (idpath _)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Univalence.