- notation fix for reducible and normal forms

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / unfold / lifts.ma

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts.ma
index 57405868f0a4979a9e6167bf976711ffb6150829..6a3c647a0cfa2b10674332c5fdd78f84fb52c192 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts.ma
@@ -112,11 +112,11 @@ qed-.
 
 (* Basic forward lemmas *****************************************************)
 
-lemma lifts_simple_dx: â\88\80T1,T2,des. â\87§*[des] T1 â\89¡ T2 â\86\92 ð\9d\95\8a[T1] â\86\92 ð\9d\95\8a[T2].
+lemma lifts_simple_dx: â\88\80T1,T2,des. â\87§*[des] T1 â\89¡ T2 â\86\92 ð\9d\90\92[T1] â\86\92 ð\9d\90\92[T2].
 #T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_dx/
 qed-.
 
-lemma lifts_simple_sn: â\88\80T1,T2,des. â\87§*[des] T1 â\89¡ T2 â\86\92 ð\9d\95\8a[T2] â\86\92 ð\9d\95\8a[T1].
+lemma lifts_simple_sn: â\88\80T1,T2,des. â\87§*[des] T1 â\89¡ T2 â\86\92 ð\9d\90\92[T2] â\86\92 ð\9d\90\92[T1].
 #T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_sn/
 qed-.