X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fsyntax%2Fteqx.ma;h=f44d4c438a43c77cf94fed157d0870088ec5722c;hp=ed581c5be2f804d0fd0bcfdda75871aeec35da23;hb=e23331eef5817eaa6c5e1c442d1d6bbb18650573;hpb=b118146b97959e6a6dde18fdd014b8e1e676a2d1

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/teqx.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/teqx.ma
index ed581c5be..f44d4c438 100644
--- 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.