Definition disassemble_attempt {x} : attempt x -> (∏ y w, y<w -> w=x -> attempt y). Proof. intros f y' y l e. exists (λ t p, f t (cons' p l e)). intros z p. use attempt_comp. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Univalence.