- we set up the support for the "bt-reduction" of Automath literature

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / computation / xprs.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/xprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/xprs.ma
index c07de4dfd5e85a22da8169908e62de15834b7e60..34e93db9d9f739669aff5f675f9ac9f2b6405062 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/xprs.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/xprs.ma
@@ -27,31 +27,31 @@ interpretation "extended parallel computation (term)"
 (* Basic eliminators ********************************************************)
 
 lemma xprs_ind: ∀h,g,L,T1. ∀R:predicate term. R T1 →
-                (â\88\80T,T2. â¦\83h, Lâ¦\84 â\8a¢ T1 â\9e¸*[g] T â\86\92 â¦\83h, Lâ¦\84 â\8a¢ T â\9e¸[g] T2 → R T → R T2) →
-                â\88\80T2. â¦\83h, Lâ¦\84 â\8a¢ T1 â\9e¸*[g] T2 → R T2.
+                (â\88\80T,T2. â¦\83h, Lâ¦\84 â\8a¢ T1 â\80¢â\9e¡*[g] T â\86\92 â¦\83h, Lâ¦\84 â\8a¢ T â\80¢â\9e¡[g] T2 → R T → R T2) →
+                â\88\80T2. â¦\83h, Lâ¦\84 â\8a¢ T1 â\80¢â\9e¡*[g] T2 → R T2.
 #h #g #L #T1 #R #HT1 #IHT1 #T2 #HT12
 @(TC_star_ind … HT1 IHT1 … HT12) //
 qed-.
 
 lemma xprs_ind_dx: ∀h,g,L,T2. ∀R:predicate term. R T2 →
-                   (â\88\80T1,T. â¦\83h, Lâ¦\84 â\8a¢ T1 â\9e¸[g] T â\86\92 â¦\83h, Lâ¦\84 â\8a¢ T â\9e¸*[g] T2 → R T → R T1) →
-                   â\88\80T1. â¦\83h, Lâ¦\84 â\8a¢ T1 â\9e¸*[g] T2 → R T1.
+                   (â\88\80T1,T. â¦\83h, Lâ¦\84 â\8a¢ T1 â\80¢â\9e¡[g] T â\86\92 â¦\83h, Lâ¦\84 â\8a¢ T â\80¢â\9e¡*[g] T2 → R T → R T1) →
+                   â\88\80T1. â¦\83h, Lâ¦\84 â\8a¢ T1 â\80¢â\9e¡*[g] T2 → R T1.
 #h #g #L #T2 #R #HT2 #IHT2 #T1 #HT12
 @(TC_star_ind_dx … HT2 IHT2 … HT12) //
 qed-.
 
 (* Basic properties *********************************************************)
 
-lemma xprs_refl: ∀h,g,L,T. ⦃h, L⦄ ⊢ T ➸*[g] T.
+lemma xprs_refl: ∀h,g,L. reflexive … (xprs h g L).
 /2 width=1/ qed.
 
 lemma xprs_strap1: ∀h,g,L,T1,T,T2.
-                   â¦\83h, Lâ¦\84 â\8a¢ T1 â\9e¸*[g] T â\86\92 â¦\83h, Lâ¦\84 â\8a¢ T â\9e¸[g] T2 â\86\92 â¦\83h, Lâ¦\84 â\8a¢ T1 â\9e¸*[g] T2.
-/2 width=3 by step/ qed. (**) (* NTypeChecker failure without trace *)
+                   â¦\83h, Lâ¦\84 â\8a¢ T1 â\80¢â\9e¡*[g] T â\86\92 â¦\83h, Lâ¦\84 â\8a¢ T â\80¢â\9e¡[g] T2 â\86\92 â¦\83h, Lâ¦\84 â\8a¢ T1 â\80¢â\9e¡*[g] T2.
+/2 width=3/ qed.
 
 lemma xprs_strap2: ∀h,g,L,T1,T,T2.
-                   â¦\83h, Lâ¦\84 â\8a¢ T1 â\9e¸[g] T â\86\92 â¦\83h, Lâ¦\84 â\8a¢ T â\9e¸*[g] T2 â\86\92 â¦\83h, Lâ¦\84 â\8a¢ T1 â\9e¸*[g] T2.
-/2 width=3 by TC_strap/ qed. (**) (* NTypeChecker failure without trace *)
+                   â¦\83h, Lâ¦\84 â\8a¢ T1 â\80¢â\9e¡[g] T â\86\92 â¦\83h, Lâ¦\84 â\8a¢ T â\80¢â\9e¡*[g] T2 â\86\92 â¦\83h, Lâ¦\84 â\8a¢ T1 â\80¢â\9e¡*[g] T2.
+/2 width=3/ qed.
 
 (* Basic inversion lemmas ***************************************************)
 (*