X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fcsuba%2Fprops.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fcsuba%2Fprops.ma;h=0dddd9cd8d5e5b5269916b65cf3b90e42b65269f;hb=639e798161afea770f41d78673c0fe3be4125beb;hp=5dab712a8b678e1a71523daaf04eddaa522f7548;hpb=15455aa487e001c643b4f46daf82612b8409f1ae;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_1/csuba/props.ma b/matita/matita/contribs/lambdadelta/basic_1/csuba/props.ma index 5dab712a8..0dddd9cd8 100644 --- a/matita/matita/contribs/lambdadelta/basic_1/csuba/props.ma +++ b/matita/matita/contribs/lambdadelta/basic_1/csuba/props.ma @@ -21,8 +21,7 @@ include "basic_1/C/fwd.ma". theorem csuba_refl: \forall (g: G).(\forall (c: C).(csuba g c c)) \def - \lambda (g: G).(\lambda (c: C).(let TMP_1 \def (\lambda (c0: C).(csuba g c0 -c0)) in (let TMP_2 \def (\lambda (n: nat).(csuba_sort g n)) in (let TMP_3 -\def (\lambda (c0: C).(\lambda (H: (csuba g c0 c0)).(\lambda (k: K).(\lambda -(t: T).(csuba_head g c0 c0 H k t))))) in (C_ind TMP_1 TMP_2 TMP_3 c))))). + \lambda (g: G).(\lambda (c: C).(C_ind (\lambda (c0: C).(csuba g c0 c0)) +(\lambda (n: nat).(csuba_sort g n)) (\lambda (c0: C).(\lambda (H: (csuba g c0 +c0)).(\lambda (k: K).(\lambda (t: T).(csuba_head g c0 c0 H k t))))) c)).