Theorem: InterpretationEmpty (FOL/NV/Program/PEG.lean)

State before:
V_N V_T : Type
R : V_N → PE V_N V_T
n : ℕ
xs : List V_T
o : Option (List V_T)
h1 : Interpretation V_N V_T R (empty, xs) (n, o)
⊢ n = 1 ∧ o = some []
Tactic:
cases h1
State after:
case empty
V_N V_T : Type
R : V_N → PE V_N V_T
xs : List V_T
⊢ 1 = 1 ∧ some [] = some []

State before:
case empty
V_N V_T : Type
R : V_N → PE V_N V_T
xs : List V_T
⊢ 1 = 1 ∧ some [] = some []
Tactic:
simp
State after:
no goals