-alias list /Coq/Lists/PolyList/Lists/list.ind#1/1
-alias AllS_assoc /Coq/Lists/TheoryList/Lists/Assoc_sec/AllS_assoc.ind#1/1
+alias list /Coq/Lists/PolyList/list.ind#1/1
+alias AllS_assoc /Coq/Lists/TheoryList/AllS_assoc.ind#1/1
+alias V /Coq/Lists/PolyList/Lists/A.var
+alias VA /Coq/Lists/TheoryList/Lists/A.var
+alias VB /Coq/Lists/TheoryList/Lists/Assoc_sec/B.var