proposition: Lemma subst_subst_term sigma1 sigma2 t : subst sigma2 (subst sigma1 t) = subst (funcomp (subst sigma2) sigma1) t.
proof: Proof. elim: t sigma1 sigma2 => /=. - done. - move=> ? IH1 ? IH2 ??. by rewrite IH1 IH2. - move=> ? IH ??. rewrite IH. congr lam. apply: ext_subst_term. case; first done. move=> ?. by rewrite /= !ren_subst_term !subst_ren_term. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect