-interpretation "Excess limsup" 'limsup e s x = (cic:/matita/limit/limsup.con e s x).
-interpretation "Excess liminf" 'liminf e s x = (cic:/matita/limit/limsup.con (cic:/matita/excess/dual_exc.con e) s x).
+interpretation "Excess limsup" 'limsup e s x = (limsup e s x).
+interpretation "Excess liminf" 'liminf e s x = (limsup (dual_exc e) s x).