proposition: Proposition inductive_implies_fixpoint (i j : G) (f g : tlist edges i j) : (tlist'_quiver_inductive _ _ f g) -> tlist'_quiver_equiv _ _ _ f g eq_refl.
proof: Proof. intro H. induction H; [ now simpl | simpl ]. exists eq_refl; 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