-interpretation "relation invertion" 'invert a =
- (cic:/matita/dama/uniform/invert_relation.con _ a).
-interpretation "relation invertion" 'invert2 a x =
- (cic:/matita/dama/uniform/invert_relation.con _ a x).
+interpretation "relation invertion" 'invert a = (invert_relation _ a).
+interpretation "relation invertion" 'invert2 a x = (invert_relation _ a x).