- ##[ ##1: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##2: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##3: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##4: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##5: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##6: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##7: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##8: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##9: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##10: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##11: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##12: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##13: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##14: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##15: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##16: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##17: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##18: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##19: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##20: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##21: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##22: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##23: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##24: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##25: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##26: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##27: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##28: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##29: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
- ##| ##30: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
+ ##[ ##1: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##2: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##3: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##4: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##5: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##6: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##7: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##8: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##9: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##10: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##11: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##12: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##13: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##14: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##15: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##16: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##17: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##18: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##19: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##20: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##21: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##22: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##23: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##24: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##25: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##26: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##27: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##28: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##29: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
+ ##| ##30: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq