proposition: Lemma source_commutation : source commutation = fob f (vertex a).
proof: Proof. uf commutation. rw source_cone_to_limit. rww vertex_cone_pushdown. app is_cone_cone_pushdown. am. rww socle_cone_pushdown. Qed.
imports: Arith nat_trans