alias id "eq_ind_r" = "cic:/Coq/Init/Logic/eq_ind_r.con".
alias id "sym_eq" = "cic:/Coq/Init/Logic/sym_eq.con".
+(*
+
theorem SKK:
\forall A:Set.
\forall app: A \to A \to A.
(inv (mult x y)) = (add (inv x) (inv y)).
intros.auto paramodulation.
qed.
+
+*)