fact: Fixpoint bitseq_of_stack (bs : bit_stack) : bitseq := match bs with | Bstack0 => [::] | Bpush0 bs' => false :: bitseq_of_stack bs' | Bpush1 bs' => true :: bitseq_of_stack bs' end.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype) fourcolor(color)