proposition: Lemma empty_function_bf: bijection_prop empty_function emptyset emptyset.
proof: Proof. have [p1 p2 p3]:= empty_function_function. split => //; split;split => //. by move => x y; rewrite p2 => /in_set0. by move => y; rewrite p3 => /in_set0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)