[STATEMENT]
lemma errMOD_igSubstAbsIPresIGWlsAbsSTR:
assumes *: "igSubstAbsIPresIGWlsAbs MOD" and **: "igWlsAbsDisj MOD"
and ***: "igWlsAbsIsInBar MOD"
shows "igSubstAbsIPresIGWlsAbsSTR (errMOD MOD)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. igSubstAbsIPresIGWlsAbsSTR (errMOD MOD)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
igSubstAbsIPresIGWlsAbs MOD
igWlsAbsDisj MOD
igWlsAbsIsInBar MOD

goal (1 subgoal):
 1. igSubstAbsIPresIGWlsAbsSTR (errMOD MOD)
[PROOF STEP]
by (simp add: errMOD_def igSubstAbsIPresIGWlsAbs_def igSubstAbsIPresIGWlsAbsSTR_def 
igWlsAbsIsInBar_def igWlsAbsDisj_def split: withERR.splits) blast