partial commit in static_2

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / syntax / teqw.ma

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/teqw.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/teqw.ma
index 1412f42b6a35c3ab6a7fe636328f05ef0768c2cc..6758d2f3d24792e06830c19049a85c8c03effd92 100644 (file)
--- 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-.