proposition: Lemma vident_axioms : forall f, Functor.axioms f -> axioms (vident f) = True.
proof: Proof. ir. app iff_eq; ir. clear H0. uf vident. ap create_axioms. uhg; dj. am. am. tv. tv. ap mor_id. ap ob_fob. am. am. rw source_id. tv. ap ob_fob; am. rw target_id; try tv; try (ap ob_fob; am). cp H7; rwi mor_facts_rw H7; uh H7; ee. rw left_id. rw right_id. tv. ap ob_fob; am. ap mor_fmor; am. rw source_fmor; try am. tv. tv. fw. fw. fw. tv. Qed.
imports: Arith functor