X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fcimp%2Fdefs.ma;fp=matitaB%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fcimp%2Fdefs.ma;h=0000000000000000000000000000000000000000;hb=88a68a9c334646bc17314d5327cd3b790202acd6;hp=b45b64b59d253f4e4da09477c9f7f609e1bbb7ab;hpb=4904accd80118cb8126e308ae098d87f8651c9f4;p=helm.git diff --git a/matitaB/matita/contribs/LAMBDA-TYPES/Basic-1/cimp/defs.ma b/matitaB/matita/contribs/LAMBDA-TYPES/Basic-1/cimp/defs.ma deleted file mode 100644 index b45b64b59..000000000 --- a/matitaB/matita/contribs/LAMBDA-TYPES/Basic-1/cimp/defs.ma +++ /dev/null @@ -1,25 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -include "Basic-1/getl/defs.ma". - -definition cimp: - C \to (C \to Prop) -\def - \lambda (c1: C).(\lambda (c2: C).(\forall (b: B).(\forall (d1: C).(\forall -(w: T).(\forall (h: nat).((getl h c1 (CHead d1 (Bind b) w)) \to (ex C -(\lambda (d2: C).(getl h c2 (CHead d2 (Bind b) w)))))))))). -