- "small step" version of "big tree" theorem proved

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / fpbs.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma
index 8d42f50bf2e753a07067bbd6b1f775b01e6e98a9..064c94f049ddac31796109c41c8209d127d0a947 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma
@@ -62,7 +62,7 @@ lemma fqus_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2
 qed.
 
 lemma cpxs_fpbs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → ⦃G, L, T1⦄ ≥[h, g] ⦃G, L, T2⦄.
-#h #g #G #L #T1 #T2 #H @(cpxs_ind … H) -T2 
+#h #g #G #L #T1 #T2 #H @(cpxs_ind … H) -T2
 /3 width=5 by fpb_cpx, fpbs_strap1/
 qed.