X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frestricted%2Flpqs_lpqs.ma;h=ad3167d6b92a6cf29987acb294f1ba4db9502270;hb=713673ecf863cb6187291f016ed4490b12a03ac0;hp=b643d3e85897deeac55de8963df49a7a8470d2d3;hpb=520d4370a540a98f5e5e1d85acfef0c982cc1e04;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/restricted/lpqs_lpqs.ma b/matita/matita/contribs/lambdadelta/basic_2/restricted/lpqs_lpqs.ma
index b643d3e85..ad3167d6b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/restricted/lpqs_lpqs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/restricted/lpqs_lpqs.ma
@@ -40,7 +40,7 @@ lemma cpqs_fwd_shift1: ∀L1,L,T1,T. L ⊢ L1 @@ T1 ➤* T →
     elim (IH … HT12) -IH -HT12 #L2 #T #HL12 #HT1 #H destruct
     lapply (lpqs_trans … HL12 (L.ⓑ{I}V2@@L2) ?) -HL12 /3 width=1/ #HL12
     @(ex3_2_intro … (⋆.ⓑ{I}V2@@L2)) [4: /2 width=3/ | skip ] <append_assoc // (**) (* explicit constructor *)
-  | #T #_ #_ #H destruct  
+  | #T #_ #_ #H destruct
   ]
 ]
 qed-.