X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Freducibility%2Fxpr.ma;h=7375349efe659651ab8659973413a664c43298a6;hb=f7386d0b74f935f07ede4be46d0489a233d68b85;hp=78dd4502ad18898bf25f799258cdb6737f89acbc;hpb=1f1ea7bb9e6c34626bcabd4c0142fcde98bcbbe5;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr.ma
index 78dd4502a..7375349ef 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr.ma
@@ -17,8 +17,10 @@ include "basic_2/reducibility/cpr.ma".
 
 (* EXTENDED PARALLEL REDUCTION ON TERMS *************************************)
 
-definition xpr: ∀h. sd h → lenv → relation term ≝
-   λh,g,L,T1,T2. L ⊢ T1 ➡ T2 ∨ ∃l. ⦃h, L⦄ ⊢ T1 •[g, l + 1] T2.
+inductive xpr (h) (g) (L) (T1) (T2): Prop ≝
+| xpr_cpr : L ⊢ T1 ➡ T2 → xpr h g L T1 T2
+| xpr_ssta: ∀l. ⦃h, L⦄ ⊢ T1 •[g, l + 1] T2 → xpr h g L T1 T2
+.
 
 interpretation
    "extended parallel reduction (term)"
@@ -26,11 +28,5 @@ interpretation
 
 (* Basic properties *********************************************************)
 
-lemma cpr_xpr: ∀h,g,L,T1,T2. L ⊢ T1 ➡ T2 → ⦃h, L⦄ ⊢ T1 ➸[g] T2.
-/2 width=1/ qed.
-
-lemma ssta_xpr: ∀h,g,L,T1,T2,l. ⦃h, L⦄ ⊢ T1 •[g, l + 1] T2 → ⦃h, L⦄ ⊢ T1 ➸[g] T2.
-/3 width=2/ qed.
-
-lemma xpr_refl: ∀h,g,L,T. ⦃h, L⦄ ⊢ T ➸[g] T.
+lemma xpr_refl: ∀h,g,L. reflexive … (xpr h g L).
 /2 width=1/ qed.