λδ-2B is released

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / fsb_csx.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma
index 5b383e05d131faf75e85fd897e49f5d0762a65da..98bed39de105e13dd752c4e238326093503e849f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma
@@ -31,7 +31,7 @@ lemma csx_fsb_fpbs: ∀h,G1,L1,T1. ⦃G1,L1⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ →
                     ∀G2,L2,T2. ⦃G1,L1,T1⦄ ≥[h] ⦃G2,L2,T2⦄ → ≥[h] 𝐒⦃G2,L2,T2⦄.
 #h #G1 #L1 #T1 #H @(csx_ind … H) -T1
 #T1 #HT1 #IHc #G2 #L2 #T2 @(fqup_wf_ind (Ⓣ) … G2 L2 T2) -G2 -L2 -T2
-#G0 #L0 #T0 #IHu #H10 
+#G0 #L0 #T0 #IHu #H10
 lapply (fpbs_csx_conf … H10) // -HT1 #HT0
 generalize in match IHu; -IHu generalize in match H10; -H10
 @(rsx_ind … (csx_rsx … HT0)) -L0