+(*CSC: the URI must disappear: there is a bug now *)
+interpretation "logical and" 'and x y = (cic:/matita/logic/connectives/And.ind#xpointer(1/1) x y).
+(*CSC: this alias should disappear. It is now required because the notation for Coq is pre-loaded *)
+alias symbol "and" (instance 0) = "logical and".
+
+theorem proj1: \forall A,B:Prop. A \land B \to A.