Semantic typing for heap_lang

In this MR I define a semantic typing judgment for heap_lang, prove all the usual typing rules, safety, and semantic typing of the symbol table example from @dreyer's POPL talk.

Some interesting differences compared to the current logrel development:

Expressions

• By building on top of heap_lang, we get the nice notations and tactics from heap_lang for free. No more De Bruijn for expressions!
• I only defined semantic types, not syntactic types. One could define syntactic types in the future and prove the fundamental theorem, but I was not too interested in doing that.
• Due to the value restriction, we need to thunk ∀ types. I thus model the type-level abstraction Λ e as λ: <>, e and the type level application e _ as e #().
• Due to step-indexing, we need to take a step to prove the typing rule for unfolding recursive types. I defined the unfold operator rec_unfold e as (λ: "x", "x") e.

Types

• By having only semantic types, I could use Coq's binders in ∀ and ∃ types, and have nice notations. So, no more De Bruijn for types either.
• I defined a type lty as a record containing a predicate over values and a prove that the predicate is persistent. Notably, I used this record in the interpretation of ∀ and ∃ types, and thus no longer have to explicitly require the type to be persistent.

Typing judgment and typing rules

• I defined the semantic typing judgment Γ ⊨ e : A as an iProp and stated all of the typing rules using -∗.
• I used type classes for operator typing (LTyUnOp, LTyBinOp) and to keep track of unboxed types (LTyUnboxed).

CC @amintimany @dfrumin @dreyer