proposition: Lemma subst_enc_list {X: Type} (f : X -> term) sigma l : (Forall (fun x => forall sigma, subst sigma (f x) = f x) l) -> subst sigma (enc_list f l) = enc_list f l.
proof: Proof. move=> H. elim: H sigma; cbn; congruence. Qed.
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.Krivine_facts) Undecidability.LambdaCalculus.Util.term_facts Undecidability.Shared.deterministic_simulation Relations List ssreflect