nelim m1;
nelim m2;
nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
nqed.
nlemma eqmcutype_to_eq : ∀m1,m2:mcu_type.(eq_mcutype m1 m2 = true) → (m1 = m2).
ncases m1;
ncases m2;
nnormalize;
- ##[ ##1,6,11,16: #H; napply (refl_eq ??)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##1,6,11,16: #H; napply refl_eq
+ ##| ##*: #H; napply (bool_destruct … H)
##]
nqed.
ncases m1;
ncases m2;
nnormalize;
- ##[ ##1,6,11,16: #H; napply (refl_eq ??)
- ##| ##*: #H; napply (mcu_type_destruct ??? H)
+ ##[ ##1,6,11,16: #H; napply refl_eq
+ ##| ##*: #H; napply (mcu_type_destruct … H)
##]
nqed.
nchange with (match MODE_DIRn n2 with [ MODE_DIRn a ⇒ n1 = a | _ ⇒ False ]);
nrewrite < H;
nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
nqed.
nlemma instr_mode_destruct_MODE_DIRn_and_IMM1 : ∀n1,n2.MODE_DIRn_and_IMM1 n1 = MODE_DIRn_and_IMM1 n2 → n1 = n2.
nchange with (match MODE_DIRn_and_IMM1 n2 with [ MODE_DIRn_and_IMM1 a ⇒ n1 = a | _ ⇒ False ]);
nrewrite < H;
nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
nqed.
nlemma instr_mode_destruct_MODE_TNY : ∀e1,e2.MODE_TNY e1 = MODE_TNY e2 → e1 = e2.
nchange with (match MODE_TNY e2 with [ MODE_TNY a ⇒ e1 = a | _ ⇒ False ]);
nrewrite < H;
nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
nqed.
nlemma instr_mode_destruct_MODE_SRT : ∀t1,t2.MODE_SRT t1 = MODE_SRT t2 → t1 = t2.
nchange with (match MODE_SRT t2 with [ MODE_SRT a ⇒ t1 = a | _ ⇒ False ]);
nrewrite < H;
nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
nqed.