proposition: Lemma set_le_2P x : C2 <=s x -> exists a b, [/\ inc a x, inc b x & a <> b].
proof: Proof. move =>[f [[ff fi] sf <-]]. move:(set2_1 C0 C1)(set2_2 C0 C1); rewrite -/C2 - sf => sa sb. exists (Vf f C0), (Vf f C1); split; try Wtac; move/(fi _ _ sa sb); fprops. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)