proposition: Lemma Exercise4_6l E F A: finite_set F -> (forall x, inc x E -> sub (A x) F) -> E46b_conc E A -> E46b_hyp E F A.
proof: Proof. move=> pa pb pc. apply: (Exercise4_6k (G := emptyset)) => //; first fprops. move=> L LE. have ->: L =emptyset. apply /set0_P; move=> y yL; case: (LE _ yL); case. rewrite cardinal_set0. apply: cle0x; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)