`{Univalence} (R : ∀ s x, P s x <-> Q s x) : A&&P = A&&Q. Proof. apply path_subalgebra. funext s x. apply (@path_universe _ _ _ (fst (R s x))). apply (equiv_equiv_iff_hprop _ _ (R s x)). Defined.
Require Import Import algebra_notations ne_list.notations. Import subalgebra_notations.