theorem para1:
\forall n,m,n1,m1:nat.
n=m \to n1 = m1 \to (n + n1) = (m + m1).
-intros. auto.
+intros. auto paramodulation.
qed.
theorem para2:
\forall n:nat. n + n = 2 * n.
-intros. auto.
-qed.
\ No newline at end of file
+intros. auto paramodulation.
+qed.