typo fixed
A semantics of BVL in terms of a conventional inductive relation.

I tried proving the bInline function correct w.r.t. this more
conventional relational semantics. I quickly realised that
the relation semantics introduces a lot of existential
quantifiers that seem to force proofs to be rather manual.
From now on I'll stick to functional versions of big-semantics
so that rewriting can be used in the correctness proofs.

I'm committing this relation semantics just as a record of this
exercise. However, this relational semantics might not be
maintained in the future.