proposition: Lemma substrate_smallest r s: (forall y, inc y r -> inc (P y) s) -> (forall y, inc y r -> inc (Q y) s) -> sub (substrate r) s.
proof: Proof. move=> h1 h2 x; case /setU2_P; move/funI_P => [z zr ->]; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)