X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fgetl%2Fgetl.ma;h=71327becf1ca702dd30b78346cfa1c1837352472;hb=de77f79d60ee3c1d30fe03469172950b557441f3;hp=19ab5606a21cfca51c4a4662c92b8220ed9bbf26;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/getl/getl.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/getl/getl.ma index 19ab5606a..71327becf 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/getl/getl.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/getl/getl.ma @@ -14,9 +14,9 @@ (* This file was automatically generated: do not edit *********************) -include "LambdaDelta-1/getl/drop.ma". +include "Basic-1/getl/drop.ma". -include "LambdaDelta-1/getl/clear.ma". +include "Basic-1/getl/clear.ma". theorem getl_conf_le: \forall (i: nat).(\forall (a: C).(\forall (c: C).((getl i c a) \to (\forall @@ -30,6 +30,9 @@ a)).(\lambda (e: C).(\lambda (h: nat).(\lambda (H0: (getl h c e)).(\lambda a) (\lambda (x: C).(\lambda (H3: (drop h O c x)).(\lambda (H4: (clear x e)).(getl_clear_conf (minus i h) x a (getl_drop_conf_ge i a c H x h O H3 H1) e H4)))) H2))))))))). +(* COMMENTS +Initial nodes: 133 +END *) theorem getl_trans: \forall (i: nat).(\forall (c1: C).(\forall (c2: C).(\forall (h: nat).((getl @@ -48,4 +51,7 @@ h) c1 c2 H e2 H5))) (\lambda (i0: nat).(\lambda (_: (((drop i0 O c2 x) \to (getl (plus i0 h) c1 e2)))).(\lambda (H4: (drop (S i0) O c2 x)).(let H_y \def (getl_drop_trans c1 c2 h H x i0 H4) in (getl_intro (plus (S i0) h) c1 e2 x H_y H3))))) i H2)))) H1)))))))). +(* COMMENTS +Initial nodes: 247 +END *)