proposition: Lemma identity_prop x: function_prop (identity x) x x.
proof: Proof. rewrite /identity /function_prop; aw; split => //; apply: function_pr. - by apply: identity_fgraph. - by rewrite identity_r; fprops. - by rewrite identity_d. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)