proposition: Lemma proc_test (x : X) : proc [L_HOAS λ y, !!(ext test) !!(enc x) y].
proof: Proof. cbn. Lproc. Qed.
imports: Undecidability.L(Computability.MuRec) Undecidability.L.Datatypes(LNat LOptions LProd) Undecidability.Synthetic(DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.L.Datatypes.List(List_basics List_nat) Datatypes