proposition: Lemma succ_inj x y: T3nf x -> T3nf y -> (T3succ x == T3succ y) = (x==y).
proof: Proof. move => nx ny;case h: (T3succ x == T3succ 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)