proposition: Lemma consts_AppL S t: consts (AppL S t) === Consts S ++ consts t.
proof: Proof. induction S; cbn; [trivial with listdb|]. rewrite IHS; now rewrite app_assoc. Qed.
imports: Morphisms Lia List Undecidability.HOU(calculus.calculus)