proposition: Lemma Lambda_subst sigma n s: sigma • (Lambda n s) = Lambda n (it n up sigma • s).
proof: Proof. induction n in sigma |-*; cbn; (eauto 2). rewrite IHn; do 3 f_equal. symmetry. eapply it_commute. Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)