milestone in basic_2, λδ-2A reconstructed

[helm.git] / helm / software / matita / nlibrary / TPTP.ma

diff --git a/helm/software/matita/nlibrary/TPTP.ma b/helm/software/matita/nlibrary/TPTP.ma
index 1254f577ce8c20024ae350f605d56ae6394fd269..3f5eefb901b2e755770c9aa2811ccddfc405e8e3 100644 (file)
--- a/helm/software/matita/nlibrary/TPTP.ma
+++ b/helm/software/matita/nlibrary/TPTP.ma
@@ -1,4 +1,4 @@
-
+(*
 universe constraint Type[0] < Type[1].
 
 ndefinition o ≝ Prop.
@@ -10,6 +10,7 @@ ninductive Or (A,B:Prop) : Prop ≝ orl : A → Or A B | orr : B → Or A B.
 ninductive True : Prop ≝ I : True.
 ninductive False : Prop ≝ .
 ninductive Not (A : Prop) : Prop ≝ abs : (A → False) → Not A.
+
 ninductive Eq (a:i) : i → Prop ≝ refl : Eq a a.
 ndefinition eq1 ≝ λT:Type[0].λp1,p2 : T → Prop. ∀x:T.And (p1 x → p2 x) (p2 x → p1 x).  
 
@@ -22,3 +23,16 @@ non associative with precedence 40 for @{'eq ? $A $B}.
 interpretation "TPTP and" 'and A B = (And A B).
 interpretation "TPTP not" 'not B = (Not B).
 interpretation "TPTP ex"  'exists f = (Exists ? f).
+*)
+include "basics/eq.ma".
+
+ndefinition o ≝ Prop.
+naxiom i : Type[0].
+
+interpretation "myeq" 'myeq T A B = (eq T A B).
+
+notation > "'Eq' term 90 A term 90 B" 
+non associative with precedence 40 for @{'myeq ? $A $B}.
+
+naxiom bool_ext : ∀P,Q: o. (P → Q) → (Q → P) → P = Q.
+naxiom f_ext_1 : ∀a,b:Type[0].∀f,g: a → b. (∀x.f x = g x) → f = g.