proposition: Lemma cone_extensionality : forall c d, is_cone c -> is_cone d -> vertex c = vertex d -> socle c = socle d -> (forall x, ob (cone_source c) x -> edge c x = edge d x) -> c = d.
proof: Proof. ir. assert (cone_source c = cone_source d). uf cone_source. rww H2. assert (cone_target c = cone_target d). uf cone_target; rww H2. uh H; uh H0; ee. uh H; uh H0. wr H; wr H0. rw H1. ap uneq. app Nat_Trans.axioms_extensionality. rw H11. rw H8. rw H4; rw H5; rw H1. reflexivity. ir. util (H3 x). uf cone_source. uf socle. rw Nat_Trans.source_target. am. am. am. Qed.
imports: Arith nat_trans