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

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

diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_aaa.ma
index 2de7cbcd8166f8b6966a37ef03e5ec8f2acb6f7d..5beb8fe1979d59110eb9611199c198b85722a439 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_aaa.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_aaa.ma
@@ -19,6 +19,6 @@ include "basic_2/computation/xprs.ma".
 
 (* Properties on atomic arity assignment for terms **************************)
 
-lemma xprs_aaa: â\88\80h,g,L,T,A. L â\8a¢ T â\81\9d A â\86\92 â\88\80U. â¦\83h, Lâ¦\84 â\8a¢ T â\9e¸*[g] U → L ⊢ U ⁝ A.
+lemma xprs_aaa: â\88\80h,g,L,T,A. L â\8a¢ T â\81\9d A â\86\92 â\88\80U. â¦\83h, Lâ¦\84 â\8a¢ T â\80¢â\9e¡*[g] U → L ⊢ U ⁝ A.
 #h #g #L #T #A #HT #U #H @(xprs_ind … H) -U // /2 width=5/
 qed.