proposition: Lemma target_edge : forall c x, ob (cone_source c) x -> is_cone c -> target (edge c x) = fob (socle c) x.
proof: Proof. ir. uf edge. rw target_ntrans. tv. uh H0; ee. am. ufi cone_source H. ufi socle H. rwi source_target H. am. uh H0; ee; am. Qed.
imports: Arith nat_trans