fact: Definition psi_succ x := if x is cons a b c _ _ then if ((a==zero) && (b==zero)) then [zero,zero, T3succ c] else [zero,zero, x] else zero.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)