eq_coerc for smart application.

[helm.git] / helm / software / matita / nlibrary / Plogic / equality.ma

diff --git a/helm/software/matita/nlibrary/Plogic/equality.ma b/helm/software/matita/nlibrary/Plogic/equality.ma
index 275ad8db8159fde3f0fbe24f48df82734be7f95c..0b4805551a345f107b7c172c58db28785be92b85 100644 (file)
--- 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.