proposition: Lemma consts_AppR s T: consts (AppR s T) === consts s ++ Consts T.
proof: Proof. induction T; cbn; [auto with listdb|]. rewrite IHT. split; intros c; simplify; intuition. Qed.
imports: Morphisms Lia List Undecidability.HOU(calculus.calculus)