proposition: Lemma identity_Lf x: identity x = Lf id x x.
proof: Proof. have aux: lf_axiom id x x by done. apply function_exten; fprops; first by apply :lf_function. by move => t; rewrite lf_source => tx; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)