fact: Definition id_Some_inl (o : option (nat + list nat)) : option (nat + list nat) := match o with | Some (inl f) => o | _ => None end.
imports: Undecidability.L.Datatypes(LNat LOptions LSum List.List_nat) Undecidability.L.Tactics.GenEncode