X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Fcompiler%2Fsigma.ma;h=491d31e006113550d0904201c69978c7461df921;hb=aba1baf85bb8e6b3ea3e66a8c2d07601066d26bc;hp=b43e4bbb1bcf10e615eafd915e7857f5b02430c6;hpb=4924f99796029eecb58e920ca7a6a366efe2373e;p=helm.git

diff --git a/helm/software/matita/contribs/assembly/compiler/sigma.ma b/helm/software/matita/contribs/assembly/compiler/sigma.ma
index b43e4bbb1..491d31e00 100755
--- a/helm/software/matita/contribs/assembly/compiler/sigma.ma
+++ b/helm/software/matita/contribs/assembly/compiler/sigma.ma
@@ -47,15 +47,3 @@ definition sigmaFst ≝
 λT:Type.λf:T → Type.λs:sigma T f.match s with [ sigma_intro x _ ⇒ x ].
 definition sigmaSnd ≝
 λT:Type.λf:T → Type.λs:sigma T f.match s return λs.f (sigmaFst ?? s) with [ sigma_intro _ x ⇒ x ].
-
-(* tripla dipendente, suggerimento \SHcy *)
-
-inductive bisigma (A,B:Type) (P:A → B → Type) : Type ≝
-    bisigma_intro: ∀x:A.∀y:B.P x y → bisigma A B P.
-
-definition bisigmaFst ≝
-λT1,T2:Type.λf:T1 → T2 → Type.λs:bisigma T1 T2 f.match s with [ bisigma_intro x _ _ ⇒ x ].
-definition bisigmaSnd ≝
-λT1,T2:Type.λf:T1 → T2 → Type.λs:bisigma T1 T2 f.match s with [ bisigma_intro _ x _ ⇒ x ].
-definition bisigmaThd ≝
-λT1,T2:Type.λf:T1 → T2 → Type.λs:bisigma T1 T2 f.match s return λs.f (bisigmaFst ??? s) (bisigmaSnd ??? s) with [ bisigma_intro _ _ x ⇒ x ].