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

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / reducibility / xpr_aaa.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_aaa.ma
index bce096e3bd80209daf73fc0c703a0840d5f63f34..98fe013478c1963ba829dd88f3ec512242f94ed4 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_aaa.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_aaa.ma
@@ -20,6 +20,6 @@ include "basic_2/reducibility/xpr.ma".
 
 (* Properties on atomic arity assignment for terms **************************)
 
-lemma xpr_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.
-#h #g #L #T #A #HT #U * [2: * ] /2 width=3/ /2 width=6/
+lemma xpr_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 * /2 width=3/ /2 width=6/
 qed.