proposition: Lemma symmetric_extend_drel_term_algebra `{!forall s, Symmetric (R s)} {s1 s2 : Sort σ} (S : CarriersTermAlgebra C s1) (T : CarriersTermAlgebra C s2) (h : ExtendDRelTermAlgebra R S T) : ExtendDRelTermAlgebra R T S.
proof: Proof. generalize dependent s2. induction S as [| u c h]; intros s2 [] p. - destruct p as [p1 p2]. induction p1. exists idpath. by symmetry. - elim p. - elim p. - destruct p as [p f]. induction p. exists idpath. intro i. apply h. apply f. Qed.
imports: HoTT.Algebra.Universal.Algebra HoTT.HSet HoTT.Classes.interfaces.canonical_names HoTT.Algebra.Universal.Homomorphism HoTT.Algebra.Universal.Congruence