new instantiate, only known bug is w.r.t. in/out scope and file matita/contribs/ng_as...

[helm.git] / helm / software / matita / nlibrary / logic / destruct_bb.ma

diff --git a/helm/software/matita/nlibrary/logic/destruct_bb.ma b/helm/software/matita/nlibrary/logic/destruct_bb.ma
index f167be39330eedbb1c23f8ebe6a5c448860eb2d1..f188bf80fc5f7addb293cdf9d1570e3882008fdf 100644 (file)
--- a/helm/software/matita/nlibrary/logic/destruct_bb.ma
+++ b/helm/software/matita/nlibrary/logic/destruct_bb.ma
@@ -41,17 +41,16 @@ definition r1 : ∀T0,T1,a0,b0,e0.T1 a0 → T1 b0 ≝
 include "logic/equality.ma".
   
 ndefinition R1 ≝ eq_rect_Type0.
-
 ndefinition R2 :
   ∀T0:Type[0].
   ∀a0:T0.
   ∀T1:∀x0:T0. a0=x0 → Type[0].
   ∀a1:T1 a0 (refl ? a0).
-  ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ??? a1 ? p0 = x1 → Type[0].
+  ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ? a0 ? a1 ? p0 = x1 → Type[0].
   ∀b0:T0.
   ∀e0:a0 = b0.
   ∀b1: T1 b0 e0.
-  ∀e1:R1 ??? a1 ? e0 = b1.
+  ∀e1:R1 ? a0 ? a1 ? e0 = b1. (* eccezine se tolgo a0 *)
   ∀so:T2 a0 (refl ? a0) a1 (refl ? a1).T2 b0 e0 b1 e1.
 #T0;#a0;#T1;#a1;#T2;#b0;#e0;#b1;#e1;#H;
 napply (eq_rect_Type0 ????? e1);
@@ -64,16 +63,16 @@ ndefinition R3 :
   ∀a0:T0.
   ∀T1:∀x0:T0. a0=x0 → Type[0].
   ∀a1:T1 a0 (refl ? a0).
-  ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ??? a1 ? p0 = x1 → Type[0].
+  ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ? a0 ? a1 ? p0 = x1 → Type[0].
   ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
-  ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ??? a1 ? p0 = x1.
-      ∀x2:T2 x0 p0 x1 p1.R2 ???? ? ? p0 ? p1 a2 = x2 → Type[0].
+  ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ? a0 ? a1 ? p0 = x1.
+      ∀x2:T2 x0 p0 x1 p1.R2 ? a0 ? a1 ? ? p0 ? p1 a2 = x2 → Type[0].
   ∀b0:T0.
   ∀e0:a0 = b0.
   ∀b1: T1 b0 e0.
-  ∀e1:R1 ??? a1 ? e0 = b1.
+  ∀e1:R1 ? a0 ? a1 ? e0 = b1.
   ∀b2: T2 b0 e0 b1 e1.
-  ∀e2:R2 ???? ? ? e0 ? e1 a2 = b2.
+  ∀e2:R2 ? a0 ? a1 ? ? e0 ? e1 a2 = b2.
   ∀so:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).T3 b0 e0 b1 e1 b2 e2.
 #T0;#a0;#T1;#a1;#T2;#a2;#T3;#b0;#e0;#b1;#e1;#b2;#e2;#H;
 napply (eq_rect_Type0 ????? e2);