`{!forall s, Transitive (R s)} {s1 s2 s3 : Sort σ} (S : CarriersTermAlgebra C s1) (T : CarriersTermAlgebra C s2) (U : CarriersTermAlgebra C s3) (h1 : ExtendDRelTermAlgebra R S T) (h2 : ExtendDRelTermAlgebra R T U) : ExtendDRelTermAlgebra R S U. Proof. generalize dependent s3. generalize dependent s2. induction S as [| u c h]; intros s2 [? d | ? d] h2 s3 [] h3; destruct h2 as [p2 P2], h3 as [p3 P3] || by (elim h2 || elim h3). - exists (p2 @ p3). rewrite transport_pp. induction p2, p3. by transitivity d. - exists (p2 @ p3). intro i. induction p2. apply (h i _ (d i)). + apply P2. + rewrite concat_1p. apply P3. Qed.
Require Import