Keeping track of locations of disambiguated ids and symbols.

[helm.git] / matitaB / matita / lib / basics / logic.ma

diff --git a/matitaB/matita/lib/basics/logic.ma b/matitaB/matita/lib/basics/logic.ma
index 1b801a14bf8f339ef9fd20ff57072edd1022d595..fd137d662a388e5a5ffdcbfd4f6e373ae2a53fb4 100644 (file)
--- a/matitaB/matita/lib/basics/logic.ma
+++ b/matitaB/matita/lib/basics/logic.ma
@@ -19,16 +19,19 @@ inductive eq (A:Type[1]) (x:A) : A → Prop ≝
     
 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
 
+
 lemma eq_rect_r:
- ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → P x p.
+ ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. x = a → Type[2]. P a (refl A a) → P x p.
  #A #a #x #p (cases p) // qed.
 
 lemma eq_ind_r :
- ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
+ ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl A a) → 
+   ∀x.∀p:eq ? x a.P x p.
  #A #a #P #p #x0 #p0; @(eq_rect_r ? ? ? p0) //; qed.
 
 lemma eq_rect_Type2_r:
-  ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
+  ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → 
+    ∀x.∀p:eq ? x a.P x p.
   #A #a #P #H #x #p (generalize in match H) (generalize in match P)
   cases p; //; qed.
 
@@ -141,7 +144,7 @@ definition R0 ≝ λT:Type[0].λt:T.t.
   
 definition R1 ≝ eq_rect_Type0.
 
-(* useless stuff
+(* useless stuff *)
 definition R2 :
   ∀T0:Type[0].
   ∀a0:T0.
@@ -216,7 +219,7 @@ definition R4 :
 @(eq_rect_Type0 ????? e3) 
 @(R3 ????????? e0 ? e1 ? e2) 
 @a4 
-qed. *)
+qed.
 
 (* TODO concrete definition by means of proof irrelevance *)
 axiom streicherK : ∀T:Type[1].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p.