proposition: Lemma nf_phi x y : T2nf x -> T2nf y -> T2nf (phi x y).
proof: Proof. move => nx ny. case (phi_cases x y); first by case => -> //=; rewrite nx ny. by move => [-> h]; rewrite /= nx T2lt0n /= nf_pred. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)