proposition: Lemma stratified_setP i (E:= stratified_set i): ordinalp i -> (forall x, inc x E <-> (W x /\ idx x <o i)).
proof: Proof. move => /Wi_coll h; exact: (choose_pr h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)