proposition: Lemma all_terms_cons P e E: all_terms P (e :: E) -> P (fst e) /\ P (snd e) /\ all_terms P E.
proof: Proof. destruct e as [s t]; intros H; cbn. specialize (H s t) as H'; cbn in H'; intuition idtac. intros ???; eapply H; cbn; intuition. Qed.
imports: List Lia Undecidability.HOU(std.std calculus.calculus unification.higher_order_unification)