X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fsyntax%2Ftweq.ma;h=3d2671a60b5af840de8bde8e573df60bb03e5884;hb=d8d00d6f6694155be5be486a8239f5953efe28b7;hp=fd31eb05e380088b9caa71efe8ca0692e7d04ad0;hpb=0fea4ed429678c3293027cfe76fdbe15cfa331cb;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/tweq.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/tweq.ma
index fd31eb05e..3d2671a60 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/tweq.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/tweq.ma
@@ -12,13 +12,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground_2/xoa/ex_1_2.ma".
+include "ground_2/xoa/ex_3_2.ma".
 include "static_2/notation/relations/approxeq_2.ma".
 include "static_2/syntax/term_weight.ma".
 
-lemma tw_le_pair_dx (I): ∀V,T. ♯{T} < ♯{②{I}V.T}.
-#I #V #T /2 width=1 by le_S_S/
-qed.
-
 (* SORT-IRRELEVANT WHD EQUIVALENCE ON TERMS *********************************)
 
 inductive tweq: relation term ≝
@@ -211,7 +209,7 @@ elim (tweq_inv_cast_sn … H) -H #W2 #U2 #HVW #HTU #H destruct
 /2 width=1 by conj/
 qed-.
 
-lemma tweq_inv_cast_sn_XY_Y: ∀T,V. ⓝV.T ≅ T → ⊥.
+lemma tweq_inv_cast_xy_y: ∀T,V. ⓝV.T ≅ T → ⊥.
 @(f_ind … tw) #n #IH #T #Hn #V #H destruct
 elim (tweq_inv_cast_sn … H) -H #X1 #X2 #_ #HX2 #H destruct -V
 /2 width=4 by/