proposition: Lemma Exercise6_5a E F: (functions E F) <=cc (sub_functions E F).
proof: Proof. apply: sub_smaller => t /functionsP [pa pb pc]. apply /sfunctionsP;split => //;rewrite pb; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)