fact: Fixpoint i_a (preds: p_env) (g:string->Z)(a:assert) {struct a}: Prop := match a with a_b e => bf' g e | a_not a => ~ i_a preds g a | pred p l => f_p preds p (lf' g l) | a_conj a1 a2 => i_a preds g a1 /\ i_a preds g a2 end.
imports: syntax little denot Bool List String ZArith