commit of the "computation" component with lazy pointwise extensions

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / reduction / llpx_lleq.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_lleq.ma
index bc8619d66e574dc0249ec3ad4bae377d58597846..e936cc5319c66f4456b8b3bc4041161cca0f5410 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_lleq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_lleq.ma
@@ -19,6 +19,9 @@ include "basic_2/reduction/llpx.ma".
 
 (* Properties on lazy equivalence for local environments ********************)
 
+lemma llpx_lrefl: ∀h,g,G,L1,L2,T,d. L1 ⋕[T, d] L2 → ⦃G, L1⦄ ⊢ ➡[h, g, T, d] L2.
+/2 width=1 by llpx_sn_lrefl/ qed-.
+
 lemma lleq_llpx_trans: ∀h,g,G,L1,L2,T,d. L1 ⋕[T, d] L2 →
                        ∀L.⦃G, L2⦄ ⊢ ➡[h, g, T, d] L → ⦃G, L1⦄ ⊢ ➡[h, g, T, d] L.
 /3 width=3 by lleq_cpx_trans, lleq_llpx_sn_trans/ qed-.