X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fsnv_da_lpr.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fsnv_da_lpr.ma;h=f65229f067ccd95a7e58bccc2d3963c36e7a38c9;hb=f5cd5870668ed096f6d93b005e2acd3bd555f3b0;hp=d706d6dc6c53a207e97146aa81e590bc672853c4;hpb=f5c6d4c41cbbdabdf998be0c4a8242849a790f1b;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma
index d706d6dc6..f65229f06 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma
@@ -73,7 +73,7 @@ fact da_cpr_lpr_aux: ∀h,g,G0,L0,T0.
     elim (snv_fwd_da … HW) #l1 #Hl1
     lapply (IH3 … HV1 … 1 … Hl0 W1 ?) /2 width=2 by fsupp_ygt, ssta_lsstas/ #HW1
     lapply (da_cpcs_aux … IH2 IH1 … Hl1 … H … HWW1) -H
-    /3 width=5 by ygt_yprs_trans, fsupp_ygt, ssta_yprs/ #H destruct
+    /3 width=5 by ygt_fpbs_trans, fsupp_ygt, ssta_fpbs/ #H destruct
     lapply (IH1 … HV1 … Hl0 … HV12 … HL12) -HV1 -Hl0 -HV12 [ /2 by fsupp_ygt/ ] #Hl0
     lapply (IH1 … Hl1 … HW2 … HL12) -Hl1 // /2 width=1 by fsupp_ygt/ -HW
     lapply (IH1 … HU1 … Hl … HU12 (L2.ⓛW2) ?) -IH1 -HU1 -Hl -HU12 [1,2: /2 by fsupp_ygt, lpr_pair/ ] -HL12 -HW2