Function first_zero_index 

pub open spec fn first_zero_index(s: Seq<bool>) -> int

{ if s.len() == 0 { 0 } else if !s[0] { 0 } else { 1 + first_zero_index(s[1..]) } }

Index of the first false bit, or s.len() if every bit is true. Defined recursively so it is deterministic and the SMT solver can unfold it.