proposition: Lemma all_terms_app P (E1 E2: eqs): all_terms P (E1 ++ E2) <-> all_terms P E1 /\ all_terms P E2.
proof: Proof. unfold all_eqs; split. - intros H; split; intros s t H'; eapply H; simplify; intuition. - intros [H1 H2] s t; simplify; intros [? % H1|? % H2]; intuition. Qed.
imports: List Lia Undecidability.HOU(std.std calculus.calculus unification.higher_order_unification)