Function lemma_is_first_zero_unique 

pub proof fn lemma_is_first_zero_unique(s: Seq<bool>, i: int, j: int)

requires

is_first_zero(s, i),

is_first_zero(s, j),

ensures

i == j,

is_first_zero is uniquely satisfied.