[STATEMENT]
lemma eVar_simp[simp]:
"eVar MOD xs x = OK (igVar MOD xs x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eVar MOD xs x = OK (igVar MOD xs x)
[PROOF STEP]
unfolding errMOD_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. igVar \<lparr>igWls = \<lambda>s eX. case eX of ERR \<Rightarrow> False | OK X \<Rightarrow> igWls MOD s X, igWlsAbs = \<lambda>(us, s) eA. case eA of ERR \<Rightarrow> False | OK A \<Rightarrow> igWlsAbs MOD (us, s) A, igVar = \<lambda>xs x. OK (igVar MOD xs x), igAbs = \<lambda>xs x eX. if eX \<noteq> ERR \<and> (\<exists>s. isInBar (xs, s) \<and> igWls MOD s (check eX)) then OK (igAbs MOD xs x (check eX)) else ERR, igOp = \<lambda>delta einp ebinp. if liftAll (\<lambda>X. X \<noteq> ERR) einp \<and> liftAll (\<lambda>A. A \<noteq> ERR) ebinp \<and> igWlsInp MOD delta (checkI einp) \<and> igWlsBinp MOD delta (checkI ebinp) then OK (igOp MOD delta (checkI einp) (checkI ebinp)) else ERR, igFresh = \<lambda>ys y eX. if eX \<noteq> ERR \<and> (\<exists>s. igWls MOD s (check eX)) then igFresh MOD ys y (check eX) else True, igFreshAbs = \<lambda>ys y eA. if eA \<noteq> ERR \<and> (\<exists>us s. igWlsAbs MOD (us, s) (check eA)) then igFreshAbs MOD ys y (check eA) else True, igSwap = \<lambda>zs z1 z2 eX. if eX \<noteq> ERR \<and> (\<exists>s. igWls MOD s (check eX)) then OK (igSwap MOD zs z1 z2 (check eX)) else ERR, igSwapAbs = \<lambda>zs z1 z2 eA. if eA \<noteq> ERR \<and> (\<exists>us s. igWlsAbs MOD (us, s) (check eA)) then OK (igSwapAbs MOD zs z1 z2 (check eA)) else ERR, igSubst = \<lambda>ys eY y eX. if eY \<noteq> ERR \<and> igWls MOD (asSort ys) (check eY) \<and> eX \<noteq> ERR \<and> (\<exists>s. igWls MOD s (check eX)) then OK (igSubst MOD ys (check eY) y (check eX)) else ERR, igSubstAbs = \<lambda>ys eY y eA. if eY \<noteq> ERR \<and> igWls MOD (asSort ys) (check eY) \<and> eA \<noteq> ERR \<and> (\<exists>us s. igWlsAbs MOD (us, s) (check eA)) then OK (igSubstAbs MOD ys (check eY) y (check eA)) else ERR\<rparr> xs x = OK (igVar MOD xs x)
[PROOF STEP]
by simp