Eager variables in Pure -> Thunk

Alluded to in #40, ThunkLang passes are unusual: `pure_to_thunk` first `Force`s all variables (which are thunks), then `thunk_let_force` attempts to detect eager variables (those that are `seq`ed) and un-`Force` them. In other words:
```
seq (var x) $ ... var x ...
--> let fresh = force (var x) in ... force (var x) ... -- pure_to_thunk
--> let fresh = force (var x) in ... var fresh ... -- thunk_let_force
```

It makes more sense to do this in one step (during `pure_to_thunk`) by tracking the eager variables currently in scope. This also avoids repeatedly `seq`ed variables: we will know that `x` is eager when processing the second `seq` in `seq (var x) $ ... seq (var x) ...`, and will not issue a second `Force` (though we would still issue the `let`-binding).

We can verify this new `pure_to_thunk` by recombining existing relations. But we should consider combining the initial `pure_to_thunk` relation and `thunk_let_forceProof$e_rel` instead. This would reduce proof bloat, and conceptually these belong together because `pure_to_thunk` handles non-strictness. We can also compile the repeated `seq`s above without the second `let`-binding. Also, if we introduce Haskell's optionally-strict bindings (i.e. "bang patterns") we can more easily produce good code, as the combined relation already tracks lazy/eager bindings.

Start with the pure_to_thunk and thunk_let_forceProof$e_rel relations, tracing how seq, Force, and let-bindings are handled. Resolve whether to track eager variables in pure_to_thunk or combine the existing relations; done should include avoiding repeated Force operations for repeated seqs and validating the resulting relation.

Written by the indexing model from the issue text.