proposition: Lemma mu_option_equiv {X} `{encodable X} s (b : X) : proc s -> mu_option s == s (mu (lam (s 0 (lam (enc true)) (enc false)))) (lam 0) (lam 0).
proof: Proof. unfold mu_option. intros Hs. now Lsimpl. Qed.
imports: Undecidability.H10(H10 dio_single dio_logic) Undecidability.L.Datatypes(LNat LOptions LSum) Undecidability.L(Tactics.LTactics Computability.MuRec Computability.Synthetic Tactics.GenEncode) Undecidability.Shared(DLW.Utils.finite DLW.Vec.vec DLW.Vec.pos) Undecidability.MuRec(MuRec recalg ra_sem_eq) Undecidability.L.Reductions.MuRec.MuRec_extract Undecidability.L.Reductions.MuRec.MuRec_extract Undecidability(MuRec_computable LVector) Undecidability.L.Util(NaryApp ClosedLAdmissible) Undecidability(LOptions)