proposition: Lemma bigfcupP' x (F : I -> {fset T}) : reflect (exists2 i : I, (i \in r) & x \in F i) (x \in \bigcup_(i <- r | true) F i).
proof: Proof. apply: (iffP idP) => [|[i ri]]; last first. by apply: fsubsetP x; rewrite bigfcup_sup. rewrite big_seq_cond; elim/big_rec: _ => [|i _ /andP[ri Pi] _ /fsetUP[|//]]. by rewrite in_fset0. by exists i; rewrite ?ri. Qed.
imports: JMeq mathcomp(all_ssreflect) mathcomp(finmap) mathcomp(classical_sets) monae_lib HB(structures) hierarchy monad_lib fail_lib state_lib trace_lib monad_transformer