proposition: Lemma EPperm_extend_M3: EPperm_M empty_function \0c.
proof: Proof. split; last by move => i j _ /clt0. have [pa pb pc]:= empty_function_function. by apply: (perm_ints NS0 _ pb pc);split => //; rewrite pc => y /in_set0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)