]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_1/getl/dec.ma
update in basic_2
[helm.git] / matita / matita / contribs / lambdadelta / basic_1 / getl / dec.ma
index dda85e7f30706b714708b4a064366d559b55778a..a8f4df8bdff85989abee7bd7d31e046524b94296 100644 (file)
@@ -16,7 +16,7 @@
 
 include "basic_1/getl/props.ma".
 
-theorem getl_dec:
+lemma getl_dec:
  \forall (c: C).(\forall (i: nat).(or (ex_3 C B T (\lambda (e: C).(\lambda 
 (b: B).(\lambda (v: T).(getl i c (CHead e (Bind b) v)))))) (\forall (d: 
 C).((getl i c d) \to (\forall (P: Prop).P)))))