X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Faprem%2Fprops.ma;h=1932956b1299d72b875ab66493ae3cd749265ac5;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=fb83210624ef7643d1de9c49b699518e030a509b;hpb=88a68a9c334646bc17314d5327cd3b790202acd6;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/aprem/props.ma b/matita/matita/contribs/lambdadelta/basic_1/aprem/props.ma
index fb8321062..1932956b1 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/aprem/props.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/aprem/props.ma
@@ -14,11 +14,11 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/aprem/fwd.ma".
+include "basic_1/aprem/fwd.ma".
 
-include "Basic-1/leq/defs.ma".
+include "basic_1/leq/fwd.ma".
 
-theorem aprem_repl:
+lemma aprem_repl:
  \forall (g: G).(\forall (a1: A).(\forall (a2: A).((leq g a1 a2) \to (\forall 
 (i: nat).(\forall (b2: A).((aprem i a2 b2) \to (ex2 A (\lambda (b1: A).(leq g 
 b1 b2)) (\lambda (b1: A).(aprem i a1 b1)))))))))
@@ -55,11 +55,8 @@ A).(leq g b1 b2)) (\lambda (b1: A).(aprem (S i0) (AHead a0 a4) b1))) (\lambda
 A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1: A).(aprem (S i0) (AHead a0 
 a4) b1)) x H7 (aprem_succ a4 x i0 H8 a0))))) H6))))))) i H4)))))))))))) a1 a2 
 H)))).
-(* COMMENTS
-Initial nodes: 621
-END *)
 
-theorem aprem_asucc:
+lemma aprem_asucc:
  \forall (g: G).(\forall (a1: A).(\forall (a2: A).(\forall (i: nat).((aprem i 
 a1 a2) \to (aprem i (asucc g a1) a2)))))
 \def
@@ -70,7 +67,4 @@ A).(aprem_zero a0 (asucc g a3)))) (\lambda (a0: A).(\lambda (a: A).(\lambda
 (i0: nat).(\lambda (_: (aprem i0 a0 a)).(\lambda (H1: (aprem i0 (asucc g a0) 
 a)).(\lambda (a3: A).(aprem_succ (asucc g a0) a i0 H1 a3))))))) i a1 a2 
 H))))).
-(* COMMENTS
-Initial nodes: 101
-END *)