fact: Definition fp1 (l0 l:ab_env) (b:bexpr)(i:instr) (f:ab_env-> a_instr*option ab_env) := match intersect_env true l b with None => (prec false_assert (mark i), Some l) | Some l' => let (i', l'') := f l' in match l'' with None => (i', None) | Some l2 => (i', Some (l0 @@ l' @@ l2)) end end.
imports: syntax little denot Bool List String ZArith axiom