proposition: Lemma setUDl : @BindLaws.left_distributive _ (fun I A => @bigcup A I) (@setU).
proof: Proof. move=> A B /= p q r; apply boolp.funext => b; rewrite boolp.propeqE; split. move=> -[a [?|?] ?]; by [left; exists a | right; exists a]. by rewrite /setU => -[[a ? ?]|[a ? ?]]; exists a => //; [left|right]. 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