3 problems solved patching the alpha-conversion of coq 7.3.1

[helm.git] / matita / contribs / LAMBDA-TYPES / Level-1 / LambdaDelta / lift1 / fwd.ma

diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift1/fwd.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift1/fwd.ma
index 3492c7ba4a79e04c0a82b0690a942db7464137de..4b548cbffbfb8ebff2ec046a43f3a70179ee7baa 100644 (file)
--- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift1/fwd.ma
+++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift1/fwd.ma
@@ -18,6 +18,8 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/lift1/fwd".
 
 include "lift1/defs.ma".
 
+include "lift/fwd.ma".
+
 theorem lift1_lref:
  \forall (hds: PList).(\forall (i: nat).(eq T (lift1 hds (TLRef i)) (TLRef 
 (trans hds i))))