proposition: Lemma SET_coUAlaw2 : forall (X : SET) (tau : Cone X F) (g : Map0'' X SET_lim), (forall (i : J) (x : X), tau i x =_S SET_lcone_tau i (g x)) -> forall x : X, g x =_S'' SET_diese tau x.
proof: Proof. intros X tau g H x; simpl in |- *. unfold Equal_NT in |- *; simpl in |- *; intro i; simpl in |- *; unfold Ext in |- *; simpl in |- *. intro e; elim e; simpl in |- *. apply Sym; apply (H i x). Qed.
imports: SET Single Limit Map0_dup1