proposition: Lemma SET_lcone_cone_law : forall (i j : J) (g : i --> j) (tau : SET_lim), SET_lcone_tau j tau =_S FMor F g (SET_lcone_tau i tau).
proof: Proof. intros i j g sigma. unfold SET_lcone_tau in |- *; simpl in |- *; unfold SET_lcone_tau_fun in |- *. apply (EqC sigma g Elt). Qed.
imports: SET Single Limit Map0_dup1