X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fprova.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fprova.ma;h=fc6c62b560d5ec3ae22c81f992481e6e6f8dad40;hb=fd0b1bb8a2cb5f57f148e6500ea2d5937082a7fa;hp=1b817c38e4a9920d9dea5919376dd2cb8c350e19;hpb=89f4301e7fa016e462fb4a01ad4b777c8f33912f;p=helm.git

diff --git a/helm/software/matita/contribs/prova.ma b/helm/software/matita/contribs/prova.ma
index 1b817c38e..fc6c62b56 100644
--- a/helm/software/matita/contribs/prova.ma
+++ b/helm/software/matita/contribs/prova.ma
@@ -26,6 +26,9 @@ alias id "or3_ind" = "cic:/matita/LAMBDA-TYPES/Level-1/Base/types/defs/or3_ind.c
 alias id "ex2_ind" = "cic:/Coq/Init/Logic/ex2_ind.con".
 alias id "ex3_2_ind" = "cic:/matita/LAMBDA-TYPES/Level-1/Base/types/defs/ex3_2_ind.con".
 alias id "subst0_gen_lift_ge" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/fwd/subst0_gen_lift_ge.con".
+alias id "or_intror" = "cic:/Coq/Init/Logic/or.ind#xpointer(1/1/2)".
+alias id "pr0_subst0_fwd" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/props/pr0_subst0_fwd.con".
+alias id "ex2_sym" = "cic:/matita/LAMBDA-TYPES/Level-1/Base/types/props/ex2_sym.con".
 
 inline procedural
    "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/props/pr0_subst0.con".