X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fsnv_lpr.ma;h=754c8da4a6e076d82199f097904d9bff24e6f1ad;hb=7e06d9d148ae04a21943377debd933a742d0c2fa;hp=5e0d2bf56c66b6030fbbcb9fbf3ad2fb16f317ec;hpb=3167db4903eea2eddc60a91cfd922be3672ce077;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma
index 5e0d2bf56..754c8da4a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma
@@ -87,7 +87,7 @@ fact snv_cpr_lpr_aux: ∀h,g,G0,L0,T0.
     lapply (snv_sta_aux … IH4 … HlV2 … HV2W3)
     /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs/ #HW3
     lapply (lsubsv_snv_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /3 width=3 by snv_bind, snv_cast/
-    @(lsubsv_abbr … l) /3 width=7 by fqup_fpbg/ #W #W0 #l0 #Hl0 #HV2W #HW20
+    @(lsubsv_beta … l) /3 width=7 by fqup_fpbg/ #W #W0 #l0 #Hl0 #HV2W #HW20
     lapply (lstas_sta_conf_pos … HV2W3 … HV2W) -HV2W #HW3W
     @(lstas_cpcs_lpr_aux … IH1 IH2 IH3 … HlW3 … HW3W … HlW2 … HW20 … HW32) //
     [ /3 width=9 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_sta_fpbs/