proposition: Lemma subst_enc_nat sigma n : subst sigma (enc_nat n) = enc_nat n.
proof: Proof. elim: n sigma; cbn; congruence. Qed.
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.Krivine_facts) Undecidability.LambdaCalculus.Util.term_facts Undecidability.Shared.deterministic_simulation Relations List ssreflect