proposition: Lemma f_p_lookup : forall m s l, f_p m s l = syntax.lookup string_dec (A:=list Z->Prop) m (fun _ => True) s l.
proof: Proof. intros m' s l; induction m'; simpl; auto. destruct a as [y p]; destruct (string_dec y s); auto. Qed.
imports: syntax little denot Bool List String ZArith axiom