proposition: Proposition tlist'_quiver_equiv_symmetric (k i j: G) (p : i = j) : forall (f : tlist edges i k) (g: tlist edges j k), tlist'_quiver_equiv k i j f g p -> tlist'_quiver_equiv k j i g f (eq_sym p).
proof: Proof. intro f; revert j p; induction f as [| i0 i1 fhead ftail]; intros j p g; destruct g as [|j0 j1 ghead gtail]. - unfold tlist'_quiver_equiv. intro H. rewrite H at 2. unfold Logic.transport_r. simpl. clear H. destruct p. reflexivity. - intro H; simpl in H. apply False_rect. destruct p; simpl in H. inversion H. - now apply False_rect. - simpl. intros [q e t]. exists (eq_sym q). + simpl. apply Equivalence_Symmetric. destruct p, q. simpl in *. assumption. + now apply IHftail, t. 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