proposition: Lemma ren_enc_term xi M : ren xi (enc_term M) = enc_term M.
proof: Proof. elim: M xi; intros; cbn; rewrite ?ren_enc_nat; congruence. Qed.
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.Krivine_facts) Undecidability.LambdaCalculus.Util.term_facts Undecidability.Shared.deterministic_simulation Relations List ssreflect