non associative with precedence 45
for @{ 'equiv $a $b }.
-interpretation "uguaglianza parziale" 'equiv x y =
- (cic:/matita/tests/decl/eq.ind#xpointer(1/1) _ x y).
+interpretation "uguaglianza parziale" 'equiv x y = (eq _ x y).
coercion cic:/matita/tests/decl/L.ind#xpointer(1/1/2).
axiom Rle: L R→L R→Prop.
axiom Rge: L R→L R→Prop.
-interpretation "real plus" 'plus x y =
- (cic:/matita/tests/decl/Rplus.con x y).
+interpretation "real plus" 'plus x y = (Rplus x y).
-interpretation "real leq" 'leq x y =
- (cic:/matita/tests/decl/Rle.con x y).
+interpretation "real leq" 'leq x y = (Rle x y).
-interpretation "real geq" 'geq x y =
- (cic:/matita/tests/decl/Rge.con x y).
+interpretation "real geq" 'geq x y = (Rge x y).
let rec elev (x:L R) (n:nat) on n: L R ≝
match n with