proposition: Lemma SET_coUAlaw1 : forall (X : SET) (tau : Cone X F) (i : J) (x : X), tau i x =_S SET_lcone_tau i (SET_diese tau x).
proof: Proof. simpl in |- *; intros X tau i x. unfold SET_lcone_tau_fun, SET_diese1 in |- *; simpl in |- *. apply Refl. Qed.
imports: SET Single Limit Map0_dup1