X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Fsubstitution%2Ftps_lift.ma;fp=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Fsubstitution%2Ftps_lift.ma;h=0f7496727b2db25de55223e8eb3f505e91ef734e;hb=d38087520d6ce1d696b28da40f3811291fc8a311;hp=35cff33723f7565bc03d2c17ef31917a1f1e94fa;hpb=016603891d57b4c6b41da6a398bf8ae466019f9e;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps_lift.ma
index 35cff3372..0f7496727 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps_lift.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps_lift.ma
@@ -35,7 +35,7 @@ qed.
 
 lemma tps_inv_refl_SO2: ∀L,T1,T2,d. L ⊢ T1 [d, 1] ≫ T2 →
                         ∀K,V. ↓[0, d] L ≡ K. 𝕓{Abst} V → T1 = T2.
-/2 width=8/ qed.
+/2 width=8/ qed-.
 
 (* Relocation properties ****************************************************)
 
@@ -256,7 +256,6 @@ qed.
                                         (le d i) -> (lt i (plus d h)) ->
 				        (EX u1 | t1 = (lift (minus (plus d h) (S i)) (S i) u1)).
 *)
-
 lemma tps_inv_lift1_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 →
                         ∀K,d,e. ↓[d, e] L ≡ K → ∀T1. ↑[d, e] T1 ≡ U1 →
                         d ≤ dt → dt ≤ d + e → d + e ≤ dt + et →