notational change of lift, drop, and gget

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / multiple / lifts_lifts.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lifts.ma
index d72f568681c082eb25961d5f8f620db2125e6f5d..739f790092e170dc969fbe92f275522fd322a9c7 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lifts.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lifts.ma
@@ -19,7 +19,7 @@ include "basic_2/multiple/lifts_lift.ma".
 (* Main properties **********************************************************)
 
 (* Basic_1: was: lift1_lift1 (left to right) *)
-theorem lifts_trans: â\88\80T1,T,des1. â\87§*[des1] T1 â\89¡ T â\86\92 â\88\80T2:term. â\88\80des2. â\87§*[des2] T ≡ T2 →
-                     â\87§*[des1 @@ des2] T1 ≡ T2.
+theorem lifts_trans: â\88\80T1,T,des1. â¬\86*[des1] T1 â\89¡ T â\86\92 â\88\80T2:term. â\88\80des2. â¬\86*[des2] T ≡ T2 →
+                     â¬\86*[des1 @@ des2] T1 ≡ T2.
 #T1 #T #des1 #H elim H -T1 -T -des1 // /3 width=3/
 qed.