X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fsyntax%2Fteqw.ma;h=6758d2f3d24792e06830c19049a85c8c03effd92;hb=98e786e1a6bd7b621e37ba7cd4098d4a0a6f8278;hp=1412f42b6a35c3ab6a7fe636328f05ef0768c2cc;hpb=b118146b97959e6a6dde18fdd014b8e1e676a2d1;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/teqw.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/teqw.ma
index 1412f42b6..6758d2f3d 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/teqw.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/teqw.ma
@@ -210,7 +210,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 → ⊥.
-@(f_ind … tw) #n #IH #T #Hn #V #H destruct
+@(wf1_ind_nlt … tw) #n #IH #T #Hn #V #H destruct
 elim (teqw_inv_cast_sn … H) -H #X1 #X2 #_ #HX2 #H destruct -V
 /2 width=4 by/
 qed-.