(* *)
(**************************************************************************)
-include "Legacy-1/definitions.ma".
+include "Legacy-1/theory.ma".
default "equality"
cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/eq.ind
interpretation "Coq 7.3.1 exists" 'exists \eta.x = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/ex.ind#xpointer(1/1) _ x).
interpretation "Coq 7.3.1 natural 'less or equal to'" 'leq x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/le.ind#xpointer(1/1) x y).
interpretation "Coq 7.3.1 natural 'less than'" 'lt x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/lt.con x y).
-interpretation "Coq 7.3.1 leibnitz's equality" 'eq x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/eq.ind#xpointer(1/1) _ x y).
+interpretation "Coq 7.3.1 leibnitz's equality" 'eq t x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/eq.ind#xpointer(1/1) t x y).
alias symbol "plus" = "Coq 7.3.1 natural plus".
alias symbol "minus" = "Coq 7.3.1 natural minus".