Hola.
Respecto a:
1) Está bien. lookup es precisamente la aplicación de la función a su argumento (de tipo Var).
2) Podría ser definida como una relación inductiva:
Inductive BEval(m:Memoria):BoolExpr->Valor->Prop :=
| evar:forall v:Var, BEval m (varExpr v) (lookup m v)
| eboolt: BEval m (boolExpr true) true
| ...
Saludos, Carlos