new definition of lleq allows to complete the proof of lemma 1000

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / fpns.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpns.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpns.ma
index beb022541e83e55ffc3570c1712a212089cdf866..6e68fef145b44ec2d7d833ca5b9c43062dadb85f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpns.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpns.ma
@@ -13,13 +13,13 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/btpredsnstar_8.ma".
-include "basic_2/relocation/lleq.ma".
+include "basic_2/substitution/lleq.ma".
 include "basic_2/computation/lpxs.ma".
 
 (* PARALLEL COMPUTATION FOR "BIG TREE" NORMAL FORMS *************************)
 
 inductive fpns (h) (g) (G) (L1) (T): relation3 genv lenv term ≝
-| fpns_intro: ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → L1 ⋕[0, T] L2 → fpns h g G L1 T G L2 T
+| fpns_intro: ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → L1 ⋕[T, 0] L2 → fpns h g G L1 T G L2 T
 .
 
 interpretation
@@ -34,6 +34,6 @@ lemma fpns_refl: ∀h,g. tri_reflexive … (fpns h g).
 (* Basic inversion lemmas ***************************************************) 
 
 lemma fpns_inv_gen: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊢ ⋕➡*[h, g] ⦃G2, L2, T2⦄ →
-                    ∧∧ G1 = G2 & ⦃G1, L1⦄ ⊢ ➡*[h, g] L2 & L1 ⋕[0, T1] L2 & T1 = T2.
+                    ∧∧ G1 = G2 & ⦃G1, L1⦄ ⊢ ➡*[h, g] L2 & L1 ⋕[T1, 0] L2 & T1 = T2.
 #h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /2 width=1 by and4_intro/
 qed-.