proposition: Lemma consts_subset_step s t: s > t -> consts t ⊆ consts s.
proof: Proof. induction 1; cbn; [|auto with listdb..]. subst. unfold beta. intros x ? % consts_subst_in; simplify. destruct H; [tauto|]. destruct H as [[|y] ?]; cbn in *; intuition. Qed.
imports: Morphisms Lia List Undecidability.HOU(calculus.calculus)