proposition: Lemma SET_diese_map_law : Map_law0'' SET_diese1.
proof: Proof. unfold Map_law0'' in |- *; intros x y H; simpl in |- *. unfold Equal_NT, SET_diese1 in |- *; simpl in |- *. unfold Ext in |- *; simpl in |- *; intros i a. elim a; simpl in |- *. apply Pres1; trivial. Qed.
imports: SET Single Limit Map0_dup1