- some confluence results for focalized reduction and computation

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / substitution / lsubs_sfr.ma

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 2b71621faf2ba690f8342347c570930034186d01..b71f25e5138b4877d49073a52009ebe56f38736f 100644 (file)
--- 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