-alias Ensemble /Coq/Sets/Ensembles/Ensembles/Ensemble.con
-alias Union /Coq/Sets/Ensembles/Ensembles/Union.ind#1/1
-alias Included /Coq/Sets/Ensembles/Ensembles/Included.con
-alias and /Coq/Init/Logic/Conjunction/and.ind#1/1
+alias U /Coq/Sets/Ensembles/Ensembles/U.var
+alias V /Coq/Sets/Powerset_facts/Sets_as_an_algebra/U.var
+alias Ensemble /Coq/Sets/Ensembles/Ensemble.con
+alias Union /Coq/Sets/Ensembles/Union.ind#1/1
+alias Included /Coq/Sets/Ensembles/Included.con
+alias and /Coq/Init/Logic/and.ind#1/1