proposition: Lemma subst_enc_eterms sigma l : subst sigma (enc_list enc_eterm l) = enc_list enc_eterm l.
proof: Proof. apply: subst_enc_list. apply /Forall_forall=> *. by apply: subst_enc_eterm. Qed.
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.Krivine_facts) Undecidability.LambdaCalculus.Util.term_facts Undecidability.Shared.deterministic_simulation Relations List ssreflect