∀ (s : Sort σ) (x : A s), hom_quotient_algebra_mapout s (class_of (Φ s) x) = f s x. Proof. reflexivity. Defined.
Require Import Basics.Notations. Require Import Import algebra_notations ne_list.notations. Import quotient_algebra_notations.