X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fs_transition%2Ffqu_tdeq.ma;h=d08dc97d2f135e83d62935d7090eeebf84719d79;hp=7deebbc611f41623f750873b0c30876408cdd0fc;hb=4173283e148199871d787c53c0301891deb90713;hpb=a67fc50ccfda64377e2c94c18c3a0d9265f651db

diff --git a/matita/matita/contribs/lambdadelta/static_2/s_transition/fqu_tdeq.ma b/matita/matita/contribs/lambdadelta/static_2/s_transition/fqu_tdeq.ma
index 7deebbc61..d08dc97d2 100644
--- a/matita/matita/contribs/lambdadelta/static_2/s_transition/fqu_tdeq.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/s_transition/fqu_tdeq.ma
@@ -17,11 +17,11 @@ include "static_2/s_transition/fqu_length.ma".
 
 (* SUPCLOSURE ***************************************************************)
 
-(* Inversion lemmas with context-free degree-based equivalence for terms ****)
+(* Inversion lemmas with context-free sort-irrelevant equivalence for terms *)
 
-fact fqu_inv_tdeq_aux: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ →
-                       G1 = G2 → |L1| = |L2| → T1 ≛[h, o] T2 → ⊥.
-#h #o #b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
+fact fqu_inv_tdeq_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ →
+                       G1 = G2 → |L1| = |L2| → T1 ≛ T2 → ⊥.
+#b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
 [1: #I #G #L #V #_ #H elim (succ_inv_refl_sn … H)
 |6: #I #G #L #T #U #_ #_ #H elim (succ_inv_refl_sn … H)
 ]
@@ -29,8 +29,8 @@ fact fqu_inv_tdeq_aux: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2
 qed-.
 
 (* Basic_2A1: uses: fqu_inv_eq *)
-lemma fqu_inv_tdeq: ∀h,o,b,G,L1,L2,T1,T2. ⦃G, L1, T1⦄ ⊐[b] ⦃G, L2, T2⦄ →
-                    |L1| = |L2| → T1 ≛[h, o] T2 → ⊥.
-#h #o #b #G #L1 #L2 #T1 #T2 #H
+lemma fqu_inv_tdeq: ∀b,G,L1,L2,T1,T2. ⦃G, L1, T1⦄ ⊐[b] ⦃G, L2, T2⦄ →
+                    |L1| = |L2| → T1 ≛ T2 → ⊥.
+#b #G #L1 #L2 #T1 #T2 #H
 @(fqu_inv_tdeq_aux … H) // (**) (* full auto fails *)
 qed-.