proposition: Lemma incl_bigcup_compat_list_pair (T K U : Type) (h1 h2 : T) (t1 : list T) (t2 : list (K * T)) (F : T -> set U) (G : K * T -> set U) k : F h1 \subset G (k, h2) -> \bigcup_(x in t1) F x \subset \bigcup_(x in t2) G x -> \bigcup_(x in h1 :: t1) F x \subset \bigcup_(x in (k, h2) :: t2) G x.
proof: Proof. intros Hs1 Hs2. intros x Hin. inv Hin. inv H. inv H0. - eexists. split. now left. eauto. - edestruct Hs2. eexists. split; eauto. destruct H0. eexists. split. now right; eauto. 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)