proposition: Lemma cocone_extensionality : forall c d, is_cocone c -> is_cocone d -> vertex c = vertex d -> cosocle c = cosocle d -> (forall x, ob (cocone_source c) x -> coedge c x = coedge d x) -> c = d.
proof: Proof. ir. assert (cocone_source c = cocone_source d). uf cocone_source. rww H2. assert (cocone_target c = cocone_target d). uf cocone_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. Qed.
imports: Arith limits