But autobatch works! Is the test still correct?
C.
intros (A B C S a w h b wb).
(* exact (h s (a b) b wb II). *)
C.
intros (A B C S a w h b wb).
(* exact (h s (a b) b wb II). *)
- autobatch new width = 5 depth = 3. (* look at h parameters! *)
+ autobatch width = 5 depth = 3. (* look at h parameters! *)
qed.
(* c'e' qualcosa di imperativo, se si cambia l'rdine delle ipotesi poi sclera *)
qed.
(* c'e' qualcosa di imperativo, se si cambia l'rdine delle ipotesi poi sclera *)
intros.
autobatch paramodulation.
try assumption.
intros.
autobatch paramodulation.
try assumption.
+ qed.
\ No newline at end of file