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

goal (1 subgoal):
 1. igAbsIPresIGWlsSTR (errMOD MOD)
[PROOF STEP]
by (fastforce simp: errMOD_def igAbsIPresIGWls_def igAbsIPresIGWlsSTR_def 
igWlsAbsIsInBar_def igWlsAbsDisj_def split: withERR.splits)