proposition: Lemma equiv_pointwise_eqs sigma E: (forall s t, (s, t) ∈ E -> sigma • s ≡ sigma • t) -> (sigma •₊ left_side E) ≡₊ (sigma •₊ right_side E).
proof: Proof. induction E as [| [s t]]; cbn; intros; [eauto|]. rewrite H; intuition idtac. rewrite IHE; intuition. Qed.
imports: List Lia Undecidability.HOU(std.std calculus.calculus unification.higher_order_unification)