- ext2_tc added

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / relocation / lexs.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma
index acfd31ed520bda019b54eb92a116a67d270f00c6..bd0a3af6b1f6e94066d47f93c415d332eb98aedb 100644 (file)
--- 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.