- letin K ≝ (eq_nat_of_byte8_mod t); clearbody K;
- letin K' ≝ (eq_mod_times_n_m_m_O (nat_of_bool t1) 256 ?); clearbody K';
- [ autobatch | ];
- autobatch paramodulation.
+ letin K ≝ (eq_nat_of_byte8_mod a); clearbody K;
+ letin K' ≝ (eq_mod_times_n_m_m_O (nat_of_bool b) 256 ?); clearbody K';
+ [ unfold;apply le_S_S;apply le_O_n| ];
+ rewrite > K' in ⊢ (? ? ? (? (? ? %) ?));
+ rewrite < K in ⊢ (? ? ? (? (? % ?) ?));
+ rewrite < plus_n_O;
+ apply K;