X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Ffdeq_fdeq.ma;h=1edc17d50d5f4065d16e7cb050bf8c5c3c0b9ad2;hp=d337f7054867d39fc3523c11f6b945e6024021ec;hb=f308429a0fde273605a2330efc63268b4ac36c99;hpb=87f57ddc367303c33e19c83cd8989cd561f3185b

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/fdeq_fdeq.ma b/matita/matita/contribs/lambdadelta/static_2/static/fdeq_fdeq.ma
index d337f7054..1edc17d50 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/fdeq_fdeq.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/fdeq_fdeq.ma
@@ -32,18 +32,18 @@ theorem fdeq_trans: tri_transitive … fdeq.
 /4 width=5 by fdeq_intro_sn, rdeq_trans, tdeq_rdeq_div, tdeq_trans/
 qed-.
 
-theorem fdeq_canc_sn: ∀G,G1,L,L1,T,T1. ⦃G, L, T⦄ ≛ ⦃G1, L1, T1⦄→
-                      ∀G2,L2,T2. ⦃G, L, T⦄ ≛ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≛ ⦃G2, L2, T2⦄.
+theorem fdeq_canc_sn: ∀G,G1,L,L1,T,T1. ⦃G,L,T⦄ ≛ ⦃G1,L1,T1⦄→
+                      ∀G2,L2,T2. ⦃G,L,T⦄ ≛ ⦃G2,L2,T2⦄ → ⦃G1,L1,T1⦄ ≛ ⦃G2,L2,T2⦄.
 /3 width=5 by fdeq_trans, fdeq_sym/ qed-.
 
-theorem fdeq_canc_dx: ∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≛ ⦃G, L, T⦄ →
-                      ∀G2,L2,T2. ⦃G2, L2, T2⦄ ≛ ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ ≛ ⦃G2, L2, T2⦄.
+theorem fdeq_canc_dx: ∀G1,G,L1,L,T1,T. ⦃G1,L1,T1⦄ ≛ ⦃G,L,T⦄ →
+                      ∀G2,L2,T2. ⦃G2,L2,T2⦄ ≛ ⦃G,L,T⦄ → ⦃G1,L1,T1⦄ ≛ ⦃G2,L2,T2⦄.
 /3 width=5 by fdeq_trans, fdeq_sym/ qed-.
 
 (* Main inversion lemmas with degree-based equivalence on terms *************)
 
-theorem fdeq_tdneq_repl_dx: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≛ ⦃G2, L2, T2⦄ →
-                            ∀U1,U2. ⦃G1, L1, U1⦄ ≛ ⦃G2, L2, U2⦄ →
+theorem fdeq_tdneq_repl_dx: ∀G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ≛ ⦃G2,L2,T2⦄ →
+                            ∀U1,U2. ⦃G1,L1,U1⦄ ≛ ⦃G2,L2,U2⦄ →
                             (T2 ≛ U2 → ⊥) → (T1 ≛ U1 → ⊥).
 #G1 #G2 #L1 #L2 #T1 #T2 #HT #U1 #U2 #HU #HnTU2 #HTU1
 elim (fdeq_inv_gen_sn … HT) -HT #_ #_ #HT