X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fpc3%2Fleft.ma;h=00e38a85accd7bc5415a1c62172cf778dc1dcb04;hb=e92710b1d9774a6491122668c8463b8658114610;hp=08d060d4ddcfb85db9cff00b127e286fbcf904de;hpb=bd5488c8eaa88e27d6e9e6c46566f1ed8f1a59b0;p=helm.git diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/left.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/left.ma index 08d060d4d..00e38a85a 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/left.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/left.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -include "pc3/props.ma". +include "LambdaDelta-1/pc3/props.ma". theorem pc3_ind_left__pc3_left_pr3: \forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr3 c t1 t2) \to