proposition: Proposition tlist'_quiver_equiv_reflexive (k i: G) : forall f : tlist edges i k, tlist'_quiver_equiv k i i f f eq_refl.
proof: Proof. intro f; induction f; [ now constructor |]. unshelve econstructor; easy. 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