proposition: Lemma subst_enc_eterm sigma P : subst sigma (enc_eterm P) = enc_eterm P.
proof: Proof. elim /Krivine_facts.eterm_ind': P sigma. move=> Ps t IH xi /=. do ? congr lam. do ? congr app. - by apply: subst_enc_list. - by apply: subst_enc_term. Qed.
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.Krivine_facts) Undecidability.LambdaCalculus.Util.term_facts Undecidability.Shared.deterministic_simulation Relations List ssreflect