proposition: Lemma incl_bigcup_compat_list_P (T U : Type) (h1 h2 : T) (t1 t2 : list T) (F G : T -> set U) (P : T -> Prop) : F h1 \subset G h2 -> P h1 -> P h2 -> \bigcup_(x in t1 :&: P) F x \subset \bigcup_(x in t2 :&: P) G x -> \bigcup_(x in (h1 :: t1) :&: P) F x \subset \bigcup_(x in (h2 :: t2) :&: P) G x.
proof: Proof. intros Hs1 Hp1 Hp2 Hs2. intros x Hin. inv Hin. inv H. inv H0. inv H. - eexists. split. constructor. now left. eauto. eauto. - edestruct Hs2. eexists. split; eauto. split. eassumption. eassumption. inv H. inv H3. eexists. split. constructor. now right; eauto. eassumption. eassumption. 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)