proposition: Lemma ren_enc_eterms xi l : ren xi (enc_list enc_eterm l) = enc_list enc_eterm l.
proof: Proof. apply: ren_enc_list. apply /Forall_forall=> *. by apply: ren_enc_eterm. Qed.
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.Krivine_facts) Undecidability.LambdaCalculus.Util.term_facts Undecidability.Shared.deterministic_simulation Relations List ssreflect