fact: Fixpoint f_p (preds : p_env) (s:string) (args:list Z) {struct preds} : Prop := match preds with (a,m)::tl => if string_dec a s then m args else f_p tl s args | nil => True end.
imports: syntax little denot Bool List String ZArith