proposition: Lemma nsv_00: S \0o \0o = \0o.
proof: Proof. rewrite (nsv_rec OS0 OS0). suff: (doubleI_rg S \0o \0o) = emptyset by move ->; rewrite osups_set0. by apply/set0_P => t/doubleI_rgP [] [y /in_set0]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)