fact: Fixpoint ab_update (l:ab_env)(s:string)(i:Ab.t) {struct l} : ab_env := match l with nil => nil | (s1,i')::tl => if string_dec s s1 then (s1,i)::tl else (s1,i')::ab_update tl s i end.
imports: syntax little denot Bool List String ZArith axiom