- ##[ ##1: napply eqinstrmode_to_eq1 ##| ##2: napply eqinstrmode_to_eq2
- ##| ##3: napply eqinstrmode_to_eq3 ##| ##4: napply eqinstrmode_to_eq4
- ##| ##5: napply eqinstrmode_to_eq5 ##| ##6: napply eqinstrmode_to_eq6
- ##| ##7: napply eqinstrmode_to_eq7 ##| ##8: napply eqinstrmode_to_eq8
- ##| ##9: napply eqinstrmode_to_eq9 ##| ##10: napply eqinstrmode_to_eq10
- ##| ##11: napply eqinstrmode_to_eq11 ##| ##12: napply eqinstrmode_to_eq12
- ##| ##13: napply eqinstrmode_to_eq13 ##| ##14: napply eqinstrmode_to_eq14
- ##| ##15: napply eqinstrmode_to_eq15 ##| ##16: napply eqinstrmode_to_eq16
- ##| ##17: napply eqinstrmode_to_eq17 ##| ##18: napply eqinstrmode_to_eq18
- ##| ##19: napply eqinstrmode_to_eq19 ##| ##20: napply eqinstrmode_to_eq20
- ##| ##21: napply eqinstrmode_to_eq21 ##| ##22: napply eqinstrmode_to_eq22
- ##| ##23: napply eqinstrmode_to_eq23 ##| ##24: napply eqinstrmode_to_eq24
- ##| ##25: napply eqinstrmode_to_eq25 ##| ##26: napply eqinstrmode_to_eq26
- ##| ##27: napply eqinstrmode_to_eq27 ##| ##28: napply eqinstrmode_to_eq28
- ##| ##29: napply eqinstrmode_to_eq29 ##| ##30: napply eqinstrmode_to_eq30
- ##| ##31: napply eqinstrmode_to_eq31 ##| ##32: napply eqinstrmode_to_eq32
- ##| ##33: napply eqinstrmode_to_eq33 ##| ##34: napply eqinstrmode_to_eq34
- ##]
-nqed.
-
-nlemma eq_to_eqinstrmode1 : ∀i2.MODE_INH = i2 → eq_instrmode MODE_INH i2 = true.
+ ##[ ##1: napply eqim_to_eq1 ##| ##2: napply eqim_to_eq2
+ ##| ##3: napply eqim_to_eq3 ##| ##4: napply eqim_to_eq4
+ ##| ##5: napply eqim_to_eq5 ##| ##6: napply eqim_to_eq6
+ ##| ##7: napply eqim_to_eq7 ##| ##8: napply eqim_to_eq8
+ ##| ##9: napply eqim_to_eq9 ##| ##10: napply eqim_to_eq10
+ ##| ##11: napply eqim_to_eq11 ##| ##12: napply eqim_to_eq12
+ ##| ##13: napply eqim_to_eq13 ##| ##14: napply eqim_to_eq14
+ ##| ##15: napply eqim_to_eq15 ##| ##16: napply eqim_to_eq16
+ ##| ##17: napply eqim_to_eq17 ##| ##18: napply eqim_to_eq18
+ ##| ##19: napply eqim_to_eq19 ##| ##20: napply eqim_to_eq20
+ ##| ##21: napply eqim_to_eq21 ##| ##22: napply eqim_to_eq22
+ ##| ##23: napply eqim_to_eq23 ##| ##24: napply eqim_to_eq24
+ ##| ##25: napply eqim_to_eq25 ##| ##26: napply eqim_to_eq26
+ ##| ##27: napply eqim_to_eq27 ##| ##28: napply eqim_to_eq28
+ ##| ##29: napply eqim_to_eq29 ##| ##30: napply eqim_to_eq30
+ ##| ##31: napply eqim_to_eq31 ##| ##32: napply eqim_to_eq32
+ ##| ##33: napply eqim_to_eq33 ##| ##34: napply eqim_to_eq34
+ ##]
+nqed.
+
+nlemma eq_to_eqim1 : ∀i2.MODE_INH = i2 → eq_im MODE_INH i2 = true.