Use the persistent function space in logical relations and add the symbol table example

• Use persistence relations for both the unary and binary logical relation
• Extend the language and type system with existential and universal quantifiers, and the FAA operation.
• Separate the proofs of the compatiblity lemmas
• Add the proof of the symbol table from Derek's talk
• Make the logical relation an iProp (it was a Prop)