proposition: Lemma succ_psi a b c: [a, b, c] != one -> T3succ [a,b,c] = cons a b c 0 one.
proof: Proof. by simpl; rewrite - all_zeroE; move /negbTE => ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)