proposition: Lemma incl_bigcup_list_tl_P (T U : Type) (h : T) (t : list T) (G : T -> set U) s (P : T -> Prop) : s \subset \bigcup_(x in t :&: P) G x -> s \subset \bigcup_(x in (h :: t) :&: P) G x.
proof: Proof. intros Hyp x Hin. eapply Hyp in Hin. inv Hin. inv H. inv H0. eexists. split. split. now right; eauto. eauto. 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)