proposition: Lemma subst_consts_AppL X Y (tau: X -> exp Y) S t: subst_consts tau (AppL S t) = AppL (map (subst_consts tau) S) (subst_consts tau t).
proof: Proof. induction S; cbn; congruence. Qed.
imports: Morphisms Lia List Undecidability.HOU(calculus.calculus)