proposition: Lemma bigcup_nil_set0_P (T U : Type) (F : T -> set U) (P : T -> Prop) : \bigcup_(x in [::] :&: P) F x <--> set0.
proof: Proof. split; intros Hin; inv Hin; eauto. inv H. inv H0. inv H. Qed.
imports: String micromega.Lia List Tactics TacticsUtil Instances Classes DependentClasses Sets Producer Generators EnumProofs Checker Decidability CheckerProofs mathcomp(ssreflect ssrfun ssrbool ssrnat eqtype seq) Ltac2(Ltac2)