proposition: Lemma for_all_relation_quotient {w : list (Sort σ)} (a b : FamilyProd A w) : for_all_2_family_prod (A/Ψ) (A/Ψ) (cong_quotient subrel) (map_family_prod (λ s, class_of (Ψ s)) a) (map_family_prod (λ s, class_of (Ψ s)) b) → for_all_2_family_prod A A Φ a b.
proof: Proof. intro F. induction w; cbn in *. - constructor. - destruct a as [x a], b as [y b], F as [Q F]. split. + apply Q; simpl; reflexivity. + by apply IHw. Qed.
imports: Colimits.Quotient Classes.interfaces.canonical_names Classes.theory.ua_quotient_algebra Classes.theory.ua_isomorphic Classes.theory.ua_first_isomorphism