proposition: Lemma tlist'_equiv_lengths (i j k : G) (f : tlist' k i) (g : tlist' k j) (p : i = j) : tlist'_quiver_equiv _ _ _ f g p -> tlist_length f = tlist_length g.
proof: Proof. revert j g p; induction f. - intros j g p H. destruct g; [ reflexivity | ]. simpl in H. destruct p. unfold Logic.transport_r in H; simpl in H; now inversion H. - intros j' g p; destruct g; [ now apply False_rect | simpl ]. intros [j_eq_j0 X]; apply eq_S; unshelve eapply IHf; [ exact j_eq_j0 | 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