proposition: Lemma source_our_mval : forall y, ob a y -> source (our_mval y) = fob otherv y.
proof: Proof. ir. uf our_mval. rw source_cone_to_limit. rw vertex_other_pt. tv. am. app is_cone_other_pt. ap is_limit_pointl. am. rw socle_other_pt. rw socle_pointl. tv. am. am. Qed.
imports: Arith colimits functor_cat