proposition: Lemma vident_point_functor : forall a b x, ob a x -> Category.axioms b -> vident (point_functor a b x) = point_trans a b (id a x).
proof: Proof. ir. assert (lem1: Category.axioms a). uh H; ee; am. rwi ob_facts_rw H; uh H; ee. ap Nat_Trans.axioms_extensionality. rw vident_axioms. tv. ap point_functor_axioms. am. am. ap point_trans_axioms. am. am. rw source_vident. rw source_point_trans. rw H3. tv. rw target_vident. rw target_point_trans. rw H4; tv. ir. rwi osource_vident H8. rwi source_point_functor H8. cp H8. rwi ob_functor_cat H8. uh H8; ee. rw ntrans_vident. rw target_point_functor. rw fob_point_functor. rw ntrans_point_trans. wr H11. rw id_fob. rww H10. am. rww H10. am. rw ob_functor_cat. uhg; ee; am. am. am. tv. am. am. am. rw source_point_functor. am. am. am. Qed.
imports: Arith nat_trans