proposition: Lemma equiv_eqs_pointwise sigma E: (sigma •₊ left_side E) ≡₊ (sigma •₊ right_side E) -> (forall s t, (s, t) ∈ E -> sigma • s ≡ sigma • t).
proof: Proof. induction E; cbn; intuition idtac; subst. all: eapply equiv_lstep_cons_inv in H; intuition. Qed.
imports: List Lia Undecidability.HOU(std.std calculus.calculus unification.higher_order_unification)