proposition: Lemma subst_as_ren M x : subst (scons (var x) var) M = ren (scons x id) M.
proof: Proof. rewrite ren_as_subst_term /=. apply: ext_subst_term. by case. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect