X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Flogic%2Fdestruct_bb.ma;h=f167be39330eedbb1c23f8ebe6a5c448860eb2d1;hb=0846ed20135a60c0230d38d07fc2e78ff7a1e9b9;hp=d3d2aadc3a7fbe3270574403ed7d18c9772eb44c;hpb=6044e9411b4f174f382e9594fadacb40bb23c175;p=helm.git

diff --git a/helm/software/matita/nlibrary/logic/destruct_bb.ma b/helm/software/matita/nlibrary/logic/destruct_bb.ma
index d3d2aadc3..f167be393 100644
--- a/helm/software/matita/nlibrary/logic/destruct_bb.ma
+++ b/helm/software/matita/nlibrary/logic/destruct_bb.ma
@@ -67,13 +67,13 @@ ndefinition R3 :
   ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ??? 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 ???? T2 x0 p0 ? p1 a2 = x2 → Type[0].
+      ∀x2:T2 x0 p0 x1 p1.R2 ???? ? ? p0 ? p1 a2 = x2 → Type[0].
   ∀b0:T0.
   ∀e0:a0 = b0.
   ∀b1: T1 b0 e0.
   ∀e1:R1 ??? a1 ? e0 = b1.
   ∀b2: T2 b0 e0 b1 e1.
-  ∀e2:R2 ???? T2 b0 e0 ? e1 a2 = b2.
+  ∀e2:R2 ???? ? ? 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);