X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Flexs.ma;h=bd0a3af6b1f6e94066d47f93c415d332eb98aedb;hb=7cf2232827c06c7e85a9bc3be005f9134d5b869d;hp=acfd31ed520bda019b54eb92a116a67d270f00c6;hpb=51b414e3a6f7404b16cab112e94f57aaa94a5239;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma
index acfd31ed5..bd0a3af6b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma
@@ -18,7 +18,6 @@ include "basic_2/syntax/lenv.ma".
 
 (* GENERIC ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****)
 
-(* Basic_2A1: includes: lpx_sn_atom lpx_sn_pair *)
 inductive lexs (RN,RP:relation3 lenv bind bind): rtmap → relation lenv ≝
 | lexs_atom: ∀f. lexs RN RP f (⋆) (⋆)
 | lexs_next: ∀f,I1,I2,L1,L2.