fact: Definition eqgs s1 s2 := match s1, s2 with | Gpush, Gpush => true | Gskip, Gskip => true | Gpop0, Gpop0 => true | Gpop1, Gpop1 => true | _, _ => false end.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype) fourcolor(color)