milestone update in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / syntax / teqx.ma

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/teqx.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/teqx.ma
index ed581c5be2f804d0fd0bcfdda75871aeec35da23..f44d4c438a43c77cf94fed157d0870088ec5722c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/teqx.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/teqx.ma
@@ -17,9 +17,6 @@ include "static_2/syntax/teqg.ma".
 
 (* SORT-IRRELEVANT EQUIVALENCE ON TERMS *************************************)
 
-definition sfull: relation2 nat nat ≝
-           λs1,s2. ⊤.
-
 definition teqx: relation term ≝
            teqg sfull.
 
@@ -29,10 +26,6 @@ interpretation
 
 (* Basic properties *********************************************************)
 
-lemma sfull_dec:
-      ∀s1,s2. Decidable (sfull s1 s2).
-/2 width=1 by or_introl/ qed.
-
 lemma teqx_pair:
       ∀V1,V2. V1 ≅ V2 → ∀T1,T2. T1 ≅ T2 →
       ∀I. ②[I]V1.T1 ≅ ②[I]V2.T2.