(s : Sort σ) (x y : A s) (P : Ψ s x y) : class_of (Φ s) x = class_of (Φ s) y. Proof. apply qglue. exact (subrel s x y P). Defined.
Require Import Import algebra_notations quotient_algebra_notations isomorphic_notations.