* Almost ready for release 0.99.1.

[helm.git] / matita / matita / lib / basics / jmeq.ma

diff --git a/matita/matita/lib/basics/jmeq.ma b/matita/matita/lib/basics/jmeq.ma
index a520ca96ff8964d0c38c7efb26b97c77605b0ace..274ce3d5b32329b4b3cbd07a70a8cf924b79f098 100644 (file)
--- a/matita/matita/lib/basics/jmeq.ma
+++ b/matita/matita/lib/basics/jmeq.ma
@@ -11,10 +11,10 @@
 
 include "basics/logic.ma".
 
-inductive Sigma: Type[1] ≝
- mk_Sigma: ∀p1: Type[0]. p1 → Sigma.
+inductive Sigma: Type[2] ≝
+ mk_Sigma: ∀p1: Type[1]. p1 → Sigma.
 
-definition p1: Sigma → Type[0].
+definition p1: Sigma → Type[1].
  #S cases S #Y #_ @Y
 qed.
 
@@ -22,7 +22,7 @@ definition p2: ∀S:Sigma. p1 S.
  #S cases S #Y #x @x
 qed.
 
-inductive jmeq (A:Type[0]) (x:A) : ∀B:Type[0]. B →Prop ≝
+inductive jmeq (A:Type[1]) (x:A) : ∀B:Type[1]. B →Prop ≝
 refl_jmeq : jmeq A x A x.
 
 notation < "hvbox(term 46 a break maction (≃) (≃\sub(t,u)) term 46 b)"
@@ -43,7 +43,7 @@ lemma K : ∀A.∀x:A.∀h:x=x. eqProp ? h (refl A x).
 qed.
 
 definition cast:
- ∀A,B:Type[0].∀E:A=B. A → B.
+ ∀A,B:Type[1].∀E:A=B. A → B.
  #A #B #E cases E #X @X
 qed.
 
@@ -57,14 +57,14 @@ qed.
 lemma gral: ∀A.∀x,y:A.
  mk_Sigma A x = mk_Sigma A y → x=y.
  #A #x #y #E lapply (tech1 ?? E)
- generalize in ⊢ (??(???%?)? → ?) #E1
- normalize in E1; >(K ?? E1) normalize
+ generalize {⊢ (??(???%?)? → ?)} #E1
+ normalize {E1}; >(K ?? E1) normalize
  #H @H
 qed.
 
 lemma jm_to_eq_sigma:
  ∀A,x,y. jmeq A x A y → mk_Sigma A x = mk_Sigma A y.
- #A #x #y #E cases E in ⊢ (???%); %
+ #A #x #y #E cases E {⊢ (???%)} %
 qed.
 
 definition curry:
@@ -77,7 +77,7 @@ qed.
 lemma G : ∀A.∀x:A.∀P:∀y:A.mk_Sigma A x = mk_Sigma A y →Type[0].
  P x (refl ? (mk_Sigma A x)) → ∀y.∀h:mk_Sigma A x = mk_Sigma A y.
   P y h.
- #A #x #P #H #y #E lapply (gral ??? E) #G generalize in match E;
+ #A #x #P #H #y #E lapply (gral ??? E) #G generalize {match E}
  @(match G
     return λy.λ_. ∀e:mk_Sigma A x = mk_Sigma A y. P y e
    with
@@ -94,20 +94,20 @@ lemma E : ∀A.∀x:A.∀P:∀y:A.jmeq A x A y→Type[0].
  #A #a #P #H #b #E letin F ≝ (jm_to_eq_sigma ??? E)
  lapply (G ?? (curry ?? P) ?? F)
   [ normalize //
-  | #H whd in H; @(H : PP ? (P b) ?) ]
+  | #H whd {H} @(H : PP ? (P b) ?) ]
 qed.
 
 lemma jmeq_elim : ∀A.∀x:A.∀P:∀y:A.jmeq A x A y→Type[0].
  P x (refl_jmeq A x) → ∀y.∀h:jmeq A x A y.P y h ≝ E.
 
-lemma jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. x≃y → x=y.
+lemma jmeq_to_eq: ∀A:Type[1]. ∀x,y:A. x≃y → x=y.
  #A #x #y #JMEQ @(jmeq_elim ? x … JMEQ) %
 qed.
 
-coercion jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. ∀p:x≃y.x=y ≝ jmeq_to_eq on _p:?≃? to ?=?.
+coercion jmeq_to_eq: ∀A:Type[1]. ∀x,y:A. ∀p:x≃y.x=y ≝ jmeq_to_eq on _p:?≃? to ?=?.
 
 lemma eq_to_jmeq:
-  ∀A: Type[0].
+  ∀A: Type[1].
   ∀x, y: A.
     x = y → x ≃ y.
   //