proposition: Lemma is_cone_cone_create2 : forall f v e, Functor.axioms f-> ob (target f) v-> (forall x, ob (source f) x -> mor (target f) (e x)) -> (forall x, ob (source f) x -> source (e x) = v) -> (forall x, ob (source f) x -> target (e x) = (fob f x)) -> (forall u, mor (source f) u -> comp (target f) (fmor f u) (e (source u)) = e (target u)) -> is_cone (cone_create2 f v e).
proof: Proof. ir. uf cone_create2. uhg; ee. ap cone_like_cone_create. rw edge_nt_cone_create. app Nat_Trans.create_axioms. uhg; ee. app constant_functor_axioms. uh H; ee; am. uh H; ee; am. am. rww source_constant_functor. rww target_constant_functor. ir. rwi source_constant_functor H5. au. ir. rwi source_constant_functor H5. rw fob_constant_functor. au. am. am. ir. rwi source_constant_functor H5. au. ir. rwi source_constant_functor H5. rww fmor_constant_functor. rww H4. rww right_id. ap H1. rww ob_target. rw H2. tv. rww ob_target. rw vertex_cone_create. uf cone_target. uf socle. rw edge_nt_cone_create. rw target_create. am. rw edge_nt_cone_create. rw source_create. rw vertex_cone_create. uf cone_source; uf cone_target; uf socle; rw edge_nt_cone_create. rw target_create. tv. Qed.
imports: Arith nat_trans