#n1; #n2; #H;
nrewrite > H;
nelim n2;
- ##[ ##2,9,10: #o; nrewrite > (eq_to_eqoct … (refl_eq …))
- ##| ##4: #t; nrewrite > (eq_to_eqbit … (refl_eq …)) ##]
+ ##[ ##4,11,12: #o; nrewrite > (eq_to_eqoct … (refl_eq …))
+ ##| ##6: #t; nrewrite > (eq_to_eqbit … (refl_eq …)) ##]
nnormalize;
napply refl_eq.
nqed.