AMBDA-TYPES: some improvements. subst now fully exploited

[helm.git] / matita / contribs / RELATIONAL / Zah / defs.ma

diff --git a/matita/contribs/RELATIONAL/Zah/defs.ma b/matita/contribs/RELATIONAL/Zah/defs.ma
index 2f9e42d4dd10b636b404ed1be16a7b3dff475dcd..83c9ceeea16771ee95c31e922bf00ee525b1fce4 100644 (file)
--- a/matita/contribs/RELATIONAL/Zah/defs.ma
+++ b/matita/contribs/RELATIONAL/Zah/defs.ma
@@ -19,7 +19,7 @@ include "logic/coimplication.ma".
 include "NPlusList/defs.ma".
 
 definition Zah \def Nat \times Nat.
-
+(*
 definition ZEq: Zah \to Zah -> Prop :=
    \lambda z1,z2.
    \forall n. ((\fst z1) + (\snd z2) == n) \liff (\fst z2) + (\snd z1) == n.
@@ -30,3 +30,4 @@ interpretation "integer equality" 'zeq x y =
 notation "hvbox(a break = b)"
   non associative with precedence 45
 for @{ 'zeq $a $b }.
+*)
\ No newline at end of file