X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fcsubt%2Fprops.ma;fp=matita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fcsubt%2Fprops.ma;h=1942b98f94e16c7aa4cf6058fd4fa4f765df3a64;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1 diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/props.ma new file mode 100644 index 000000000..1942b98f9 --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/props.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "LambdaDelta-1/csubt/defs.ma". + +theorem csubt_refl: + \forall (g: G).(\forall (c: C).(csubt g c c)) +\def + \lambda (g: G).(\lambda (c: C).(C_ind (\lambda (c0: C).(csubt g c0 c0)) +(\lambda (n: nat).(csubt_sort g n)) (\lambda (c0: C).(\lambda (H: (csubt g c0 +c0)).(\lambda (k: K).(\lambda (t: T).(csubt_head g c0 c0 H k t))))) c)). +