]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/fwd.ma
LambdaDelta-1 regenerated as a subdevel ov LAMBDA-TYPES
[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / LambdaDelta-1 / getl / fwd.ma
index 0f32449475c5a55e04cdb75f9be77f55f8810248..13f96107e870a673f5a7fa673e5541a4c1719a59 100644 (file)
 
 (* This file was automatically generated: do not edit *********************)
 
-include "getl/defs.ma".
+include "LambdaDelta-1/getl/defs.ma".
 
-include "drop/fwd.ma".
+include "LambdaDelta-1/drop/fwd.ma".
 
-include "clear/fwd.ma".
+include "LambdaDelta-1/clear/fwd.ma".
 
 theorem getl_gen_all:
  \forall (c1: C).(\forall (c2: C).(\forall (i: nat).((getl i c1 c2) \to (ex2