proposition: Lemma succ_psi2 u (x := [zero,zero,u]) : (forall a' b' c', T3nf c' -> x < [a',b',c'] -> (psi_succ x) <= [a',b',c']).
proof: Proof. move => a' b' c' nc'. rewrite /T3le lt_omega2 /x /psi_succ eqxx /=; rewrite lt_omega2. case pa: ((a' == zero) && (b' == zero)). rewrite lt_succ_le_4 //; case/orP; last by move => ->; rewrite orbT. by move => /eqP ->; move/andP: pa => [/eqP -> /eqP ->]; rewrite eqxx. by move => h;rewrite succ_psi_lt // ? orbT //; rewrite T3eqE andbA pa. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)