proposition: Lemma subst_consts_AppR X Y (tau: X -> exp Y) s T: subst_consts tau (AppR s T) = AppR (subst_consts tau s) (map (subst_consts tau) T).
proof: Proof. induction T; cbn; congruence. Qed.
imports: Morphisms Lia List Undecidability.HOU(calculus.calculus)