proposition: Lemma sub_in_bij (D1' : pred T1) : {subset D1 <= D1'} -> {in D1', bijective f} -> {in D1, bijective f}.
proof: Proof. by move=> subD [g' fK g'K]; exists g' => x; move/subD; [apply: fK | apply: g'K]. Qed.
imports: ssreflect ssrfun