X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fsubstitution%2Flsubs_sfr.ma;h=b71f25e5138b4877d49073a52009ebe56f38736f;hb=9c09a0b1f8801e40612eef429b82fc6dbae01b85;hp=2b71621faf2ba690f8342347c570930034186d01;hpb=ea83c19f4cac864dd87eb059d8aeb2343eba480f;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/lsubs_sfr.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/lsubs_sfr.ma
index 2b71621fa..b71f25e51 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/substitution/lsubs_sfr.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/lsubs_sfr.ma
@@ -43,6 +43,11 @@ elim (lsubs_inv_abbr2 … H ?) -H // <minus_plus_m_m #X #HLX #H destruct
 lapply (HL … HLX) -HL -HLX /2 width=1/
 qed.
 
+lemma sfr_abbr_O: ∀L,V. ≽[0,1] L.ⓓV.
+#L #V
+@(sfr_abbr … 0) //
+qed.
+
 lemma sfr_skip: ∀I,L,V,d,e. ≽ [d, e] L → ≽ [d + 1, e] L.ⓑ{I}V.
 #I #L #V #d #e #HL #K #H
 elim (lsubs_inv_skip2 … H ?) -H // <minus_plus_m_m #J #X #W #HLX #H destruct