fact: Fixpoint T2limit x := if x is cons a b n c then if ([a,b]==one) then false else (c== zero) || T2limit c else false.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)