proposition: Lemma sup_Oalpha_succ x: T3nf x -> sup_of id (T3succ x) x.
proof: Proof. move => nx;split. - done. - by move => y nf; rewrite lt_succ_le_3. - by move => z nz zx; exists x; rewrite succ_lt nx zx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)