{w : list (Sort σ)} : ∀ (P : FamilyProd carriers_quotient_algebra w → Type) `{!∀ a, IsHProp (P a)} (dclass : ∀ x, P (map_family_prod (λ s, class_of (Φ s)) x)) (a : FamilyProd carriers_quotient_algebra w), P a := match w with | nil => λ P _ dclass 'tt, dclass tt | s :: w' => λ P _ dclass a, Quotient_ind_hprop (Φ s) (λ a, ∀ b, P (a,b)) (λ a, (λ c, P (class_of (Φ s) a, c)) (λ c, dclass (a, c))) (fst a) (snd a) end.
Require Import Basics.Notations. Require Import Import algebra_notations ne_list.notations. Import quotient_algebra_notations.