proposition: Lemma cone_target_cone_transform : forall u c, cone_transformable u c -> cone_target (cone_transform u c) = cone_target c.
proof: Proof. ir. uf cone_target. rww socle_cone_transform. uh H; ee. wr H1. rww target_source. Qed.
imports: Arith nat_trans