proposition: Lemma subst_consts_Lambda Y Z (zeta: Y -> exp Z) k s: subst_consts zeta (Lambda k s) = Lambda k (subst_consts (zeta >> ren (plus k)) s).
proof: Proof. induction k in zeta |-*; cbn; asimpl; trivial. f_equal. rewrite IHk. f_equal. f_equal. asimpl. fext; intros x; unfold funcomp; f_equal; fext; intros ?. unfold shift; simplify; f_equal; lia. Qed.
imports: Morphisms Lia List Undecidability.HOU(calculus.calculus)