]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_llor.ma
some renaming and some typos corrected ...
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / multiple / llpx_sn_llor.ma
index bc65d200238ffaaff8e06fed192053bf67c8e9ab..e5933d4c7358fabc4db7604a9b609d30007a1137 100644 (file)
@@ -18,7 +18,7 @@ include "basic_2/multiple/lleq_alt.ma".
 
 (* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****)
 
-(* Inversion lemmas on poinwise union for local environments ****************)
+(* Inversion lemmas on pointwise union for local environments ****************)
 
 lemma llpx_sn_llor_fwd_sn: ∀R. (∀L. reflexive … (R L)) →
                            ∀L1,L2,T,d. llpx_sn R d T L1 L2 →