proposition: Lemma normal_form_enc_list {X: Type} (f : X -> term) l : (forall x, normal_form (f x)) -> normal_form (enc_list f l).
proof: Proof. move=> Hf. elim: l; by do ? constructor. Qed.
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.Krivine_facts) Undecidability.LambdaCalculus.Util.term_facts Undecidability.Shared.deterministic_simulation Relations List ssreflect