proposition: Lemma peval_next t b : ieval t b = None -> exists2 b1, b1 \in moves t b & eval t b = sflip (eval (flip t) b1).
proof: Proof. move=> Hi; have := liveness t b; rewrite evalE Hi => /(@sym_equal _ _ _). rewrite eqxx => /idP /(bigsmin_ex (eval (flip t))) [c H1c H2c]. by exists c => //=; rewrite H2c. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)