Definition assemble_attempt {x} : (∏ y y', y<y' -> y'=x -> attempt y) -> attempt x. Proof. intros fs. use tpair. - intros y [[|n] c]. + apply H. intros z lzy. exact (fs z y lzy c z nil). + induction c as [s [t [c' [l' e']]]]. exact (fs s t l' e' y (n,,c')). - intros y [[|n] c]. + reflexivity. + use attempt_comp. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Univalence.