fact: Definition cell_of_next_bin_ops_spec'' (level : nat) (cell : option nat) (str : String) offset idx := (cell = Some idx -> index_points_to_binop offset idx str /\ paren_balanced_hiding' (take idx (drop offset str)) level) /\ (cell = None -> paren_balanced' (take idx (drop offset str)) level -> index_not_points_to_binop offset idx str).
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.ZArith.ZArith Fiat.Common Fiat.Common.List.Operations Fiat.Common.List.ListFacts Fiat.Common.SetoidInstances Fiat.Parsers.Reachable.ParenBalanced.Core Fiat.Parsers.StringLike.Core Fiat.Parsers.StringLike.Properties Fiat.Parsers.StringLike.FirstChar Fiat.Parsers.Refinement.BinOpBrackets.ParenBalanced