proposition: Lemma in_bigcup_list_cons_P (T U : Type) (h : T) (t : seq T) (G : T -> set U) (z : U) (P : T -> Prop) : (\bigcup_(x in ((h :: t) :&: P)) G x) z -> G h z /\ P h \/ (\bigcup_(x in t :&: P) G x) z.
proof: Proof. intros Hin. inv Hin. inv H. inv H0; eauto. inv H; eauto. right. eexists; split; eauto. split; eauto. 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)