X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fsty1%2Fcnt.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fsty1%2Fcnt.ma;h=54354378cd5c6677f8029556bdb11c4e22af5dd1;hb=8de8cf8adfa6fcda91047eb2c25535893ede046a;hp=4a8aa1a3058fe30f13168e7458be3a95e45356cb;hpb=d2caaf419cb6c92cb5ca8615f8eac4e12f3ab728;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_1/sty1/cnt.ma b/matita/matita/contribs/lambdadelta/basic_1/sty1/cnt.ma index 4a8aa1a30..54354378c 100644 --- a/matita/matita/contribs/lambdadelta/basic_1/sty1/cnt.ma +++ b/matita/matita/contribs/lambdadelta/basic_1/sty1/cnt.ma @@ -18,7 +18,7 @@ include "basic_1/sty1/props.ma". include "basic_1/cnt/props.ma". -theorem sty1_cnt: +lemma sty1_cnt: \forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t: T).((sty0 g c t1 t) \to (ex2 T (\lambda (t2: T).(sty1 g c t1 t2)) (\lambda (t2: T).(cnt t2)))))))