X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1A%2Fpc3%2Fdefs.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1A%2Fpc3%2Fdefs.ma;h=22679602b1edabde6ca3a54f612d99d76ac0cd5c;hb=d2545ffd201b1aa49887313791386add78fa8603;hp=0000000000000000000000000000000000000000;hpb=57ae1762497a5f3ea75740e2908e04adb8642cc2;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_1A/pc3/defs.ma b/matita/matita/contribs/lambdadelta/basic_1A/pc3/defs.ma new file mode 100644 index 000000000..22679602b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_1A/pc3/defs.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||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_1A/pr3/defs.ma". + +definition pc3: + C \to (T \to (T \to Prop)) +\def + \lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(ex2 T (\lambda (t: T).(pr3 +c t1 t)) (\lambda (t: T).(pr3 c t2 t))))). + +inductive pc3_left (c: C): T \to (T \to Prop) \def +| pc3_left_r: \forall (t: T).(pc3_left c t t) +| pc3_left_ur: \forall (t1: T).(\forall (t2: T).((pr2 c t1 t2) \to (\forall +(t3: T).((pc3_left c t2 t3) \to (pc3_left c t1 t3))))) +| pc3_left_ux: \forall (t1: T).(\forall (t2: T).((pr2 c t1 t2) \to (\forall +(t3: T).((pc3_left c t1 t3) \to (pc3_left c t2 t3))))). +