From: Enrico Tassi Date: Thu, 15 Apr 2010 14:02:02 +0000 (+0000) Subject: bool_ext on 'o' not on 'Prop' (they are convertible, but discrimination X-Git-Tag: make_still_working~2920 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4682ca97a527e269be028e9f275c09c116511253;p=helm.git bool_ext on 'o' not on 'Prop' (they are convertible, but discrimination trees do not compare up to conversion) From: tassi --- 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.