some renaming and some typos corrected ...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / multiple / llpx_sn.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn.ma
index 692039c1150264e1d310bcff83dc071626b10e4a..f0d8bbcfe69c32e140e5b294ca8141b7c6bd1d08 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn.ma
@@ -145,7 +145,7 @@ lemma llpx_sn_fwd_pair_sn: ∀R,I,L1,L2,V,T,d. llpx_sn R d (②{I}V.T) L1 L2 →
 #R * /2 width=4 by llpx_sn_fwd_flat_sn, llpx_sn_fwd_bind_sn/
 qed-.
 
-(* Basic_properties *********************************************************)
+(* Basic properties *********************************************************)
 
 lemma llpx_sn_refl: ∀R. (∀L. reflexive … (R L)) → ∀T,L,d. llpx_sn R d T L L.
 #R #HR #T #L @(f2_ind … rfw … L T) -L -T