-alias eq /Coq/Init/Logic/Equality/eq.ind#1/1
-alias refl_equal /Coq/Init/Logic/Equality/eq.ind#1/1/1
-alias eq_ind /Coq/Init/Logic/Equality/eq_ind.con
-alias eq_ind_r /Coq/Init/Logic/Logic_lemmas/eq_ind_r.con
+alias eq /Coq/Init/Logic/eq.ind#1/1
+alias refl_equal /Coq/Init/Logic/eq.ind#1/1/1
+alias eq_ind /Coq/Init/Logic/eq_ind.con
+alias eq_ind_r /Coq/Init/Logic/eq_ind_r.con