- we commit just the components before "reducibility"

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / restricted / lpqs_lpqs.ma

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 b643d3e85897deeac55de8963df49a7a8470d2d3..ad3167d6b92a6cf29987acb294f1ba4db9502270 100644 (file)
--- 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-.