From 4682ca97a527e269be028e9f275c09c116511253 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 15 Apr 2010 14:02:02 +0000 Subject: [PATCH] bool_ext on 'o' not on 'Prop' (they are convertible, but discrimination trees do not compare up to conversion) From: tassi --- helm/software/matita/nlibrary/TPTP.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/matita/nlibrary/TPTP.ma b/helm/software/matita/nlibrary/TPTP.ma index 326b673fc..3f5eefb90 100644 --- a/helm/software/matita/nlibrary/TPTP.ma +++ b/helm/software/matita/nlibrary/TPTP.ma @@ -34,5 +34,5 @@ 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: Prop. (P → Q) → (Q → P) → P = Q. +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. -- 2.39.2