+set "baseuri" "cic:/Coq/".
+
(* aritmetic operators *)
interpretation "Coq's natural plus" 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
interpretation "Coq's logical and" 'and x y = (cic:/Coq/Init/Logic/and.ind#xpointer(1/1) x y).
interpretation "Coq's logical or" 'or x y = (cic:/Coq/Init/Logic/or.ind#xpointer(1/1) x y).
interpretation "Coq's logical not" 'not x = (cic:/Coq/Init/Logic/not.con x).
-interpretation "Coq's exists" 'exists x y = (cic:/Coq/Init/Logic/ex.ind#xpointer(1/1) x y).
+interpretation "Coq's exists" 'exists \eta.x = (cic:/Coq/Init/Logic/ex.ind#xpointer(1/1) _ x).
(* relational operators *)