proposition: Lemma for_all_2_family_prod_trace_congruence {w : SymbolType σ} (a b : FamilyProd (A&&P) (dom_symboltype w)) (R : for_all_2_family_prod (A&&P) (A&&P) cong_trace a b) : for_all_2_family_prod A A Φ (map_family_prod i a) (map_family_prod i b).
proof: Proof. Proof with try assumption. induction w... destruct a as [x a], b as [y b], R as [C R]. split... apply IHw... Qed.
imports: HSet Colimits.Quotient Classes.interfaces.canonical_names Classes.theory.ua_isomorphic Classes.theory.ua_subalgebra Classes.theory.ua_quotient_algebra