- nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H));
- nletin H1 ≝ (andb_true_true_l ?? H);
- nrewrite > (eqbool_to_eq x12 y12 (andb_true_true_r ?? (andb_true_true_l ?? H)));
- nletin H2 ≝ (andb_true_true_l ?? H1);
- nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H2));
- nletin H3 ≝ (andb_true_true_l ?? H2);
- nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H3));
- nletin H4 ≝ (andb_true_true_l ?? H3);
- nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H4));
- nletin H5 ≝ (andb_true_true_l ?? H4);
- nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H5));
- nletin H6 ≝ (andb_true_true_l ?? H5);
- nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H6));
- nletin H7 ≝ (andb_true_true_l ?? H6);
- nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H7));
- nletin H8 ≝ (andb_true_true_l ?? H7);
- nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H8));
- nletin H9 ≝ (andb_true_true_l ?? H8);
- nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H9));
- nletin H10 ≝ (andb_true_true_l ?? H9);
- nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H10));
- nletin H11 ≝ (andb_true_true_l ?? H10);
- nrewrite > (eqb8_to_eq ?? (andb_true_true_r ?? H11));
- nrewrite > (eqb8_to_eq ?? (andb_true_true_l ?? H11));
- napply (refl_eq ??).
+ nrewrite > (eqbool_to_eq … (andb_true_true_r … H));
+ nletin H1 ≝ (andb_true_true_l … H);
+ nrewrite > (eqbool_to_eq x12 y12 (andb_true_true_r … (andb_true_true_l … H)));
+ nletin H2 ≝ (andb_true_true_l … H1);
+ nrewrite > (eqbool_to_eq … (andb_true_true_r … H2));
+ nletin H3 ≝ (andb_true_true_l … H2);
+ nrewrite > (eqbool_to_eq … (andb_true_true_r … H3));
+ nletin H4 ≝ (andb_true_true_l … H3);
+ nrewrite > (eqbool_to_eq … (andb_true_true_r … H4));
+ nletin H5 ≝ (andb_true_true_l … H4);
+ nrewrite > (eqbool_to_eq … (andb_true_true_r … H5));
+ nletin H6 ≝ (andb_true_true_l … H5);
+ nrewrite > (eqw16_to_eq … (andb_true_true_r … H6));
+ nletin H7 ≝ (andb_true_true_l … H6);
+ nrewrite > (eqw16_to_eq … (andb_true_true_r … H7));
+ nletin H8 ≝ (andb_true_true_l … H7);
+ nrewrite > (eqw16_to_eq … (andb_true_true_r … H8));
+ nletin H9 ≝ (andb_true_true_l … H8);
+ nrewrite > (eqw16_to_eq … (andb_true_true_r … H9));
+ nletin H10 ≝ (andb_true_true_l … H9);
+ nrewrite > (eqw16_to_eq … (andb_true_true_r … H10));
+ nletin H11 ≝ (andb_true_true_l … H10);
+ nrewrite > (eqb8_to_eq … (andb_true_true_r … H11));
+ nrewrite > (eqb8_to_eq … (andb_true_true_l … H11));
+ napply refl_eq.