proposition: Lemma all_terms_cons_iff P e E: all_terms P (e :: E) <-> P (fst e) /\ P (snd e) /\ all_terms P E.
proof: Proof. unfold all_eqs; cbn; split. - eauto using all_terms_cons. - intros (? & ? & ?) ? ? [->|H']; firstorder idtac. Qed.
imports: List Lia Undecidability.HOU(std.std calculus.calculus unification.higher_order_unification)