autobatch width = 5 depth = 3. (* look at h parameters! *)
qed.
-(* c'e' qualcosa di imperativo, se si cambia l'rdine delle ipotesi poi sclera *)
+(* c'e' qualcosa di imperativo, se si cambia l'ordine delle ipotesi poi sclera *)
theorem prova2:
\forall A,B,C:Prop. (* SE METTO SET NON VA *)
\forall a:B -> A.
\forall b:B.
A=B.
intros.
- autobatch paramodulation.
+ autobatch.
try assumption.
qed.
\ No newline at end of file