X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fsyntax%2Fteqw.ma;h=b9515a0333692637022acb7ea59310788c46b926;hp=6758d2f3d24792e06830c19049a85c8c03effd92;hb=156d974ad89aa04a086fdf9d332c8b04adf279fd;hpb=8fe4dc148d50a0352313633bea61441bc817afbf

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/teqw.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/teqw.ma
index 6758d2f3d..b9515a033 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/teqw.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/teqw.ma
@@ -14,6 +14,7 @@
 
 include "ground/xoa/ex_1_2.ma".
 include "ground/xoa/ex_3_2.ma".
+include "ground/arith/wf1_ind_plt.ma".
 include "static_2/notation/relations/tildeminus_2.ma".
 include "static_2/syntax/term_weight.ma".
 
@@ -210,7 +211,7 @@ elim (teqw_inv_cast_sn … H) -H #W2 #U2 #HVW #HTU #H destruct
 qed-.
 
 lemma teqw_inv_cast_xy_y: ∀T,V. ⓝV.T ≃ T → ⊥.
-@(wf1_ind_nlt … tw) #n #IH #T #Hn #V #H destruct
+@(wf1_ind_plt … tw) #p #IH #T #Hp #V #H destruct
 elim (teqw_inv_cast_sn … H) -H #X1 #X2 #_ #HX2 #H destruct -V
 /2 width=4 by/
 qed-.