From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 15 Dec 2009 08:04:26 +0000 (+0000)
Subject: eq_coerc for smart application.
X-Git-Tag: make_still_working~3164
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e588f626df2898792cc9c0372f6d67602ca720fc;p=helm.git

eq_coerc for smart application.
---

diff --git a/helm/software/matita/nlibrary/Plogic/equality.ma b/helm/software/matita/nlibrary/Plogic/equality.ma
index 275ad8db8..0b4805551 100644
--- a/helm/software/matita/nlibrary/Plogic/equality.ma
+++ b/helm/software/matita/nlibrary/Plogic/equality.ma
@@ -14,24 +14,28 @@
 
 include "logic/pts.ma".
 
-ninductive peq (A:Type[0]) (x:A) : A \to Prop \def
+ninductive peq (A:Type[3]) (x:A) : A \to Prop \def
     refl_peq : peq A x x.
-    
+
 interpretation "leibnitz's equality" 'eq t x y = (peq t x y).
- 
-ntheorem rewrite_l: ∀A.∀x.∀P:A → Prop. P x → ∀y. x = y → P y.
+
+ntheorem rewrite_l: ∀A:Type[3].∀x.∀P:A → Prop. P x → ∀y. x = y → P y.
 #A; #x; #P; #Hx; #y; #Heq;ncases Heq;nassumption.
-nqed.
+nqed. 
 
-ntheorem sym_peq: ∀A.∀x,y:A. x = y → y = x.
+ntheorem sym_peq: ∀A:Type[3].∀x,y:A. x = y → y = x.
 #A; #x; #y; #Heq; napply (rewrite_l A x (λz.z=x)); 
 ##[ @; ##| nassumption; ##]
 nqed.
 
-ntheorem rewrite_r: ∀A.∀x.∀P:A → Prop. P x → ∀y. y = x → P y.
+ntheorem rewrite_r: ∀A:Type[3].∀x.∀P:A → Prop. P x → ∀y. y = x → P y.
 #A; #x; #P; #Hx; #y; #Heq;ncases (sym_peq ? ? ?Heq);nassumption.
 nqed.
 
+ntheorem eq_coerc: ∀A,B:Type[2].A→(A=B)→B.
+#A; #B; #Ha; #Heq;nelim Heq; nassumption.
+nqed.
+
 (*
 theorem eq_rect':
  \forall A. \forall x:A. \forall P: \forall y:A. x=y \to Type.