proposition: Lemma subst_enc_state ts ctx t sigma : subst sigma (enc_state ts ctx t) = enc_state ts ctx t.
proof: Proof. by rewrite /= ?simpl_term. Qed.
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.Krivine_facts) Undecidability.LambdaCalculus.Util.term_facts Undecidability.Shared.deterministic_simulation Relations List ssreflect