- Define several versios of bind and return for the relational
  interpretation
- Use those operations to prove some compatibility lemmas
  without unfolding the definitions
- Get rid of the definition unfolding in a part of the stack
  refinement proof

+ add some discussion in comments.org

- Use the type of literals in `val`
- Notation for `match`
- "Better" coercions

- Add more binary ops to the language
- An example refinement for module types

Modify the logical relation judment to include an environment Δ that
contains a list of semantic types to interpret free type variables.

- Change the types in the examples slightly
- Use notations in the examples
- Modify some tactics to make the proofs more smooth

In the interpretation of recursive types

- Remove commented out code
- Pull std++ related lemmas into a separate file

Following the advice of Amin Timany
generalize all the compatibility lemmas
at the same time by declaring a mask E in a Section.

Dan Frumin authored May 11, 2017 and Dan Frumin committed Jul 03, 2017

We are switich away from De Bruijn indices because
1) it's hard to read terms with De Bruijn indices
2) they are making lots of things slower

And improve the proof of the fundamental property

A new formulation allows for doing more work inside HOSL.

Γ ⊨ e ≤log≤ e' : τ <=>
∀ Δ vvs ρ,
  spec_ctx ρ -∗
  □ ⟦ Γ ⟧* Δ vvs -∗
  ⟦ τ ⟧ₑ Δ (e.[env_subst (vvs.*1)], e'.[env_subst (vvs.*2)])

Slightly generalize the way tac_tp_bind works and rewrite the
fundamental property for F_mu_ref_conc using tp_ tactics

sans examples

This reverts commit 15005661.

This reverts commit efe1b574.