Custom Rules for Unquoting

Option 1: custom unquoting rules, based on unifying inside quotes

says(Alice, { Food(chocolate) } )
truthTeller(Alice)
says(?person, { ?x(?y) } ) & truthTeller(?person) => ?x(?y)
------------
Food(chocolate)

We can skip {...}, but we still need an alternate name for the logical connectives

Pro: nice and simple

Con: how to handle arbitrary structure of statements?

Con: lets user naively allow paradoxes of self-reference:

true(?x) => ?x

Doesn't really need HOL, though I used HOL syntax here for simplicity.

This is pretty much cwm's approach