proposition: Proposition tlist'_quiver_equiv_transitive (k i1 i2 i3: G) : forall (f : tlist edges i1 k) (g : tlist edges i2 k) (h : tlist edges i3 k) (p : i1 = i2) (q : i2 = i3), tlist'_quiver_equiv k i1 i2 f g p -> tlist'_quiver_equiv k i2 i3 g h q-> tlist'_quiver_equiv k i1 i3 f h (eq_trans p q).
proof: Proof. intro f; revert i2 i3. induction f as [ | i0 i1 fhead ftail ]; [ intros i2 i3 g h p q equiv1 equiv2; destruct p, q; simpl in *; destruct equiv1; now simpl in equiv2 |]. intros i2 i3 g h p q equiv1 equiv2. destruct g as [ | j0 j1 ghead gtail ]; [ now apply False_rect |]. simpl in equiv1. destruct equiv1 as [j_eq_j0 fhead_eq_ghead]. destruct h as [ | k0 k1 hhead htail]; [ now apply False_rect |]. simpl; simpl in equiv2; destruct equiv2 as [j1_eq_k1 gtail_eq_htail]. unshelve esplit; [ exact (eq_trans j_eq_j0 j1_eq_k1) | |]. - destruct j1_eq_k1, p, q, j_eq_j0. unfold Logic.transport_r in *. simpl Logic.transport in *. now apply (@Equivalence_Transitive _ _ _ _ ghead). - unshelve eapply IHftail; [ exact gtail | assumption | assumption ]. Defined.
imports: Category.Lib Category.Lib.TList Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Theory.Adjunction Category.Theory.Universal.Arrow Category.Instance.StrictCat Category.Construction.Groupoid Category.Construction.Opposite Category.Construction.Product Category.Instance.Sets