proposition: Lemma succ_inj x y: T2nf x -> T2nf y -> (T2succ x == T2succ y) = (x==y).
proof: Proof. move => nx ny;case h: (T2succ x == T2succ y). by rewrite - (pred_succ nx) (eqP h) (pred_succ ny) eqxx. by case hh: (x==y) => //; rewrite -h (eqP hh) eqxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)