-interpretation "Lattice meet" 'meet = (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_mcarr.con _)).
-interpretation "Lattice meet_refl" 'meet_refl = (cic:/matita/lattice/sl_meet_refl.con (cic:/matita/lattice/latt_mcarr.con _)).
-interpretation "Lattice meet_comm" 'meet_comm = (cic:/matita/lattice/sl_meet_comm.con (cic:/matita/lattice/latt_mcarr.con _)).
-interpretation "Lattice meet_assoc" 'meet_assoc = (cic:/matita/lattice/sl_meet_assoc.con (cic:/matita/lattice/latt_mcarr.con _)).
-interpretation "Lattice strong_extm" 'strong_extm = (cic:/matita/lattice/sl_strong_extm.con (cic:/matita/lattice/latt_mcarr.con _)).
-interpretation "Lattice le_to_eqm" 'le_to_eqm = (cic:/matita/lattice/sl_le_to_eqm.con (cic:/matita/lattice/latt_mcarr.con _)).
-interpretation "Lattice lem" 'lem = (cic:/matita/lattice/sl_lem.con (cic:/matita/lattice/latt_mcarr.con _)).
-interpretation "Lattice join" 'join = (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_jcarr.con _)).
-interpretation "Lattice join_refl" 'join_refl = (cic:/matita/lattice/sl_meet_refl.con (cic:/matita/lattice/latt_jcarr.con _)).
-interpretation "Lattice join_comm" 'join_comm = (cic:/matita/lattice/sl_meet_comm.con (cic:/matita/lattice/latt_jcarr.con _)).
-interpretation "Lattice join_assoc" 'join_assoc = (cic:/matita/lattice/sl_meet_assoc.con (cic:/matita/lattice/latt_jcarr.con _)).
-interpretation "Lattice strong_extm" 'strong_extj = (cic:/matita/lattice/sl_strong_extm.con (cic:/matita/lattice/latt_jcarr.con _)).
-interpretation "Lattice le_to_eqj" 'le_to_eqj = (cic:/matita/lattice/sl_le_to_eqm.con (cic:/matita/lattice/latt_jcarr.con _)).
-interpretation "Lattice lej" 'lej = (cic:/matita/lattice/sl_lem.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice meet" 'meet = (sl_meet (latt_mcarr _)).
+interpretation "Lattice meet_refl" 'meet_refl = (sl_meet_refl (latt_mcarr _)).
+interpretation "Lattice meet_comm" 'meet_comm = (sl_meet_comm (latt_mcarr _)).
+interpretation "Lattice meet_assoc" 'meet_assoc = (sl_meet_assoc (latt_mcarr _)).
+interpretation "Lattice strong_extm" 'strong_extm = (sl_strong_extm (latt_mcarr _)).
+interpretation "Lattice le_to_eqm" 'le_to_eqm = (sl_le_to_eqm (latt_mcarr _)).
+interpretation "Lattice lem" 'lem = (sl_lem (latt_mcarr _)).
+interpretation "Lattice join" 'join = (sl_meet (latt_jcarr _)).
+interpretation "Lattice join_refl" 'join_refl = (sl_meet_refl (latt_jcarr _)).
+interpretation "Lattice join_comm" 'join_comm = (sl_meet_comm (latt_jcarr _)).
+interpretation "Lattice join_assoc" 'join_assoc = (sl_meet_assoc (latt_jcarr _)).
+interpretation "Lattice strong_extm" 'strong_extj = (sl_strong_extm (latt_jcarr _)).
+interpretation "Lattice le_to_eqj" 'le_to_eqj = (sl_le_to_eqm (latt_jcarr _)).
+interpretation "Lattice lej" 'lej = (sl_lem (latt_jcarr _)).