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

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..fa341e425 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-.