proposition: Lemma edge_cone_pushdown : forall f c x, ob (cone_source c) x -> is_cone c -> edge (cone_pushdown f c) x = fmor f (edge c x).
proof: Proof. ir. uf edge. rw edge_nt_cone_pushdown. rw ntrans_htrans_left. tv. rww osource_edge_nt. Qed.
imports: Arith nat_trans