proposition: Proposition fixpoint_implies_inductive (i j : G) (f g : tlist edges i j) : tlist'_quiver_equiv _ _ _ f g eq_refl -> (tlist'_quiver_inductive _ _ f g).
proof: Proof. revert g; induction f. - intros g H. simpl in H; unfold Logic.transport_r in H; simpl in H; destruct H. constructor. - intro g; destruct g; [ now apply False_rect |]. intro H. simpl in H; destruct H as [q t t0]. destruct q. constructor. + apply IHf. assumption. + unfold Logic.transport_r in t. simpl in t. exact 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