X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Funfold%2Fdelift_tpss.ma;h=662ae567fed348d1997cbad36f03fc8f1ce36b04;hb=08cb57944c0df08611d4f35d286e46c0d13e4813;hp=cebcf828ea1c4e944ab56971ba7b71e002c8e8b0;hpb=9245402674a791dfdb943902f8288d742088c854;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_tpss.ma
index cebcf828e..662ae567f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_tpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_tpss.ma
@@ -89,4 +89,4 @@ qed.
 
 lemma tps_delift_trans_eq: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 →
                            ∀T. L ⊢ ▼*[d, e] U2 ≡ T → L ⊢ ▼*[d, e] U1 ≡ T.
-/3 width=3/ qed.                            
+/3 width=3/ qed.