proposition: Lemma normal_form_enc_eterms Ps : normal_form (enc_list enc_eterm Ps).
proof: Proof. by apply: normal_form_enc_list. Qed.
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.Krivine_facts) Undecidability.LambdaCalculus.Util.term_facts Undecidability.Shared.deterministic_simulation Relations List ssreflect