X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Flpxs.ma;h=8b08043fd92fc72f293d742cfee028e9f9c10d21;hb=1604f2ee65c57eefb7c6b3122eab2a9f32e0552d;hp=507e0c3effa0153a61415a01301eaf7438839d41;hpb=47a745462a714af9d65cea7b61af56524bd98fa1;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma
index 507e0c3ef..8b08043fd 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma
@@ -25,6 +25,11 @@ interpretation
    "uncounted parallel rt-computation (local environment)"
    'PRedTySnStar h G L1 L2 = (lpxs h G L1 L2).
 
+(* Basic properties *********************************************************)
+
+lemma lpxs_refl: ∀h,G. reflexive … (lpxs h G).
+/2 width=1 by lex_refl/ qed.
+
 (* Basic inversion lemmas ***************************************************)
 
 lemma lpxs_inv_bind_sn: ∀h,G,I1,L2,K1. ⦃G, K1.ⓘ{I1}⦄ ⊢⬈*[h] L2 →