proposition: Lemma Exercise6_33y: Ex6_33_conc.
proof: Proof. case: Exercise6_33x; set T := Imf _; set q := E6_33_Q => ra rb rc. exists (Vfs X T), q. move: Exercise6_33d =>[iX sX _]. move: Exercise6_33q =>[_ _ _ N0c _]. have sNc: sub N c by apply: sub_trans N0c; case: Exercise6_33t. have sTc: sub T c by apply: (sub_trans ra sNc). have stX: sub T (source X) by ue. split. - move => t. move/(Vf_image_P (proj1 iX) stX) => [u uT ->]. by apply: Exercise6_33d1; apply: sTc. - move: (cardinal_image stX iX); rewrite rb=> ->; apply:Exercise6_33b. - move => i j /(Vf_image_P (proj1 iX) stX) [u uT ->]. move /(Vf_image_P (proj1 iX) stX) =>[v vT ->] ns. apply: rc => //; dneg ww; ue. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)