X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fpr3%2Fpr1.ma;h=04878c2b983bdbd8613dd687023fed9292bb9513;hb=cc6fcb70ca4f3cf01205ed722d75a2fdb2aaf779;hp=77bb9bc5916fbcf12dd3a93e9b31e1ff2a99ce80;hpb=639e798161afea770f41d78673c0fe3be4125beb;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_1/pr3/pr1.ma b/matita/matita/contribs/lambdadelta/basic_1/pr3/pr1.ma index 77bb9bc59..04878c2b9 100644 --- a/matita/matita/contribs/lambdadelta/basic_1/pr3/pr1.ma +++ b/matita/matita/contribs/lambdadelta/basic_1/pr3/pr1.ma @@ -18,7 +18,7 @@ include "basic_1/pr3/defs.ma". include "basic_1/pr1/fwd.ma". -theorem pr3_pr1: +lemma pr3_pr1: \forall (t1: T).(\forall (t2: T).((pr1 t1 t2) \to (\forall (c: C).(pr3 c t1 t2)))) \def