fact: Fixpoint f_star (n:nat)(r:env)(i:instr){struct n} :option(env*instr) := match n with 0%nat => Some(r,i) | S n => if eq_skip i then Some(r,i) else bind2 (f_sos r i) (fun r' i' => f_star n r' i') end.
imports: ZArith List syntax Lia