proposition: Lemma normal_form_enc_eterm P : normal_form (enc_eterm P).
proof: Proof. elim /Krivine_facts.eterm_ind': P. move=> ?? H /=. do ? constructor; [|done]. elim: H; by do ? constructor. Qed.
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.Krivine_facts) Undecidability.LambdaCalculus.Util.term_facts Undecidability.Shared.deterministic_simulation Relations List ssreflect