fact: Fixpoint to_a1 (l:ab_env)(ignored:list string) {struct l} : assert := match l with nil => to_assert bot (anum 0) | (s,v)::tl => if str_in_list s ignored then to_a1 tl ignored else let (ps, l) := to_syn v in a_conj (to_assert v (avar s)) (to_a1 tl (s::ignored)) end.
imports: syntax little denot Bool List String ZArith axiom