[1: simplify in A'; rewrite > cmp_refl in A'; simplify in A';
destruct A'; rewrite < count_O_mem in H1;
rewrite > Hcut in H1; simplify in H1; destruct H1;
|2: simplify; rewrite > cmp_refl; reflexivity;]
|2: intros (Ul1); lapply (H Ul1); unfold Not; intros (A); apply Hletin;
intros (r Mrl1); lapply (A r);
[1: simplify in A'; rewrite > cmp_refl in A'; simplify in A';
destruct A'; rewrite < count_O_mem in H1;
rewrite > Hcut in H1; simplify in H1; destruct H1;
|2: simplify; rewrite > cmp_refl; reflexivity;]
|2: intros (Ul1); lapply (H Ul1); unfold Not; intros (A); apply Hletin;
intros (r Mrl1); lapply (A r);