proposition: Lemma subst_var_term s : subst var s = s.
proof: Proof. elim: s. - done. - move=> ? IH1 ? IH2 /=. by rewrite IH1 IH2. - move=> ? IH /=. congr lam. rewrite -[RHS]IH. apply: ext_subst_term. by case. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect