X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Ftopology%2Figft.ma;h=a6d430cf1f59c31330efe23bacd333ab222528dd;hb=50ab627986cbf241262e5969a757b1c6c95166f4;hp=81aefd555f02c320104e47f3d272fbf5301c6673;hpb=6677f4b55d7d949ab7b8f7133f701bcc1593bbeb;p=helm.git diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma index 81aefd555..a6d430cf1 100644 --- a/helm/software/matita/nlibrary/topology/igft.ma +++ b/helm/software/matita/nlibrary/topology/igft.ma @@ -14,7 +14,7 @@ by S.Berardi and S. Valentini. The tutorial is by Enrico Tassi. The tutorial spends a considerable amount of effort in defining notations that resemble the ones used in the original paper. We believe -this a important part of every formalization, not only for the aesthetic +this is a important part of every formalization, not only from the aesthetic point of view, but also from the practical point of view. Being consistent allows to follow the paper in a pedantic way, and hopefully to make the formalization (at least the definitions and proved @@ -63,7 +63,7 @@ implements two unusual input facilities: - ∀ can be typed with `\Forall` - λ can be typed with `\lambda` - ≝ can be typed with `\def` or `:=` - - → can be typed with `to` or `->` + - → can be typed with `\to` or `->` - some symbols have variants, like the ≤ relation and ≼, ≰, ⋠. The user can cycle between variants typing one of them and then @@ -71,20 +71,43 @@ implements two unusual input facilities: example W has Ω, 𝕎 and 𝐖, L has Λ, 𝕃, and 𝐋, F has Φ, … Variants are listed in the aforementioned TeX/UTF-8 table. +Pressing `F1` opens the Matita manual. + CIC (as implemented in Matita) in a nutshell -------------------------------------------- -... +CIC is a full and functional Pure Type System (all products do exist, +and their sort is is determined by the target) with an impedicative sort +Prop and a predicative sort Type. The environment can be populated with +well typed definitions or theorems, (co)inductive types validating positivity +conditions and recursive functions provably total by simple syntactical +analysis (recursive call on structurally smaller subterms). Co-recursive +functions can be defined as well, and must satisfy a dual condition, that is +performing the recursive call only after having generated a constructor (a piece +of output). + +The λ-calculus is equipped with a pattern matching construct (match) on inductive +types defined in the environment that combined with the definable total +structural recursive functions allows to define eliminators (or constructors) +for (co)inductive types. The λ-calculus is also equipped with explicitly types +local definitions (let in) that in the degenerate case work as casts (i.e. +the type annotation `(t : T)` is implemented as `let x : T ≝ t in x`). + +Types are compare up to conversion. Since types may depend on terms, conversion +involves β-reduction, δ-reduction (definition unfolding), ζ-reduction (local +definition unfolding), ι-reduction (pattern matching simplification), +μ-reduction (recursive function computation) and ν-reduction (co-fixpoint +computation). -Type is a set equipped with the Id equality (i.e. an intensional, +Since we are going to formalize constructive and predicative mathematics +in an intensional type theory like CIC, we try to establish some terminology. +Type is the sort of sets equipped with the Id equality (i.e. an intensional, not quotiented set). We will avoid using Leibnitz equality Id, thus we will explicitly equip a set with an equality when needed. We will call this structure `setoid`. Note that we will -attach the infix = symbols only to the equality of a setoid, +attach the infix = symbol only to the equality of a setoid, not to Id. -... - We write Type[i] to mention a Type in the predicative hierarchy of types. To ease the comprehension we will use Type[0] for sets, and Type[1] for classes. @@ -92,8 +115,6 @@ and Type[1] for classes. For every Type[i] there is a corresponding level of predicative propositions CProp[i]. -CIC is also equipped with an impredicative sort Prop that we will not -use in this tutorial. The standard library and the `include` command ---------------------------------------------- @@ -103,11 +124,11 @@ are part of the standard library of Matita. These notions come with some standard notation attached to them: -- A ∪ B `A \cup B` -- A ∩ B `A \cap B` -- A ≬ B `A \between B` -- x ∈ A `x \in A` -- Ω^A, that is the type of the subsets of A, `\Omega ^ A` +- A ∪ B can be typed with `A \cup B` +- A ∩ B can be typed with `A \cap B` +- A ≬ B can be typed with `A \between B` +- x ∈ A can be typed with `x \in A` +- Ω^A, that is the type of the subsets of A, can be typed with `\Omega ^ A` The `include` command tells Matita to load a part of the library, in particular the part that we will use can be loaded as follows: @@ -116,26 +137,6 @@ D*) include "sets/sets.ma". -(*HIDE*) -(* move away *) -nlemma subseteq_intersection_l: ∀A.∀U,V,W:Ω^A.U ⊆ W ∨ V ⊆ W → U ∩ V ⊆ W. -#A; #U; #V; #W; *; #H; #x; *; #xU; #xV; napply H; nassumption; -nqed. - -nlemma subseteq_union_l: ∀A.∀U,V,W:Ω^A.U ⊆ W → V ⊆ W → U ∪ V ⊆ W. -#A; #U; #V; #W; #H; #H1; #x; *; #Hx; ##[ napply H; ##| napply H1; ##] nassumption; -nqed. - -nlemma subseteq_intersection_r: ∀A.∀U,V,W:Ω^A.W ⊆ U → W ⊆ V → W ⊆ U ∩ V. -#A; #U; #V; #W; #H1; #H2; #x; #Hx; @; ##[ napply H1; ##| napply H2; ##] nassumption; -nqed. - -ninductive sigma (A : Type[0]) (P : A → CProp[0]) : Type[0] ≝ - sig_intro : ∀x:A.P x → sigma A P. - -interpretation "sigma" 'sigma \eta.p = (sigma ? p). -(*UNHIDE*) - (*D Some basic results that we will use are also part of the sets library: @@ -541,18 +542,18 @@ D*) nlet corec fish_rec (A:Ax) (U: Ω^A) (P: Ω^A) (H1: P ⊆ U) (H2: ∀a:A. a ∈ P → ∀j: 𝐈 a. 𝐂 a j ≬ P): ∀a:A. ∀p: a ∈ P. a ⋉ U ≝ ?. - (** screenshot "def-fish-rec-1". *) -#a; #p; napply cfish; (** screenshot "def-fish-rec-2". *) + (** screenshot "def-fish-rec-1". *) +#a; #p; napply cfish; (** screenshot "def-fish-rec-2". *) ##[ nchange in H1 with (∀b.b∈P → b∈U); (** screenshot "def-fish-rec-2-1". *) - napply H1; (** screenshot "def-fish-rec-3". *) + napply H1; (** screenshot "def-fish-rec-3". *) nassumption; -##| #i; ncases (H2 a p i); (** screenshot "def-fish-rec-5". *) +##| #i; ncases (H2 a p i); (** screenshot "def-fish-rec-5". *) #x; *; #xC; #xP; (** screenshot "def-fish-rec-5-1". *) - @; (** screenshot "def-fish-rec-6". *) + @; (** screenshot "def-fish-rec-6". *) ##[ napply x - ##| @; (** screenshot "def-fish-rec-7". *) + ##| @; (** screenshot "def-fish-rec-7". *) ##[ napply xC; - ##| napply (fish_rec ? U P); (** screenshot "def-fish-rec-9". *) + ##| napply (fish_rec ? U P); (** screenshot "def-fish-rec-9". *) nassumption; ##] ##] @@ -662,7 +663,7 @@ ndefinition cover_equation : ∀A:Ax.∀U,X:Ω^A.CProp[0] ≝ λA,U,X. ntheorem coverage_cover_equation : ∀A,U. cover_equation A U (◃U). #A; #U; #a; @; #H; -##[ nelim H; #b; (* manca clear *) +##[ nelim H; #b; ##[ #bU; @1; nassumption; ##| #i; #CaiU; #IH; @2; @ i; #c; #cCbi; ncases (IH ? cCbi); ##[ #E; @; napply E; @@ -755,25 +756,32 @@ The paper defines the image as > Im[d(a,i)] = { d(a,i,j) | j : D(a,i) } -but this cannot be ..... MAIL +but this not so formal notation poses some problems. The image is +often used as the left hand side of the ⊆ predicate > Im[d(a,i)] ⊆ V -Allora ha una comoda interpretazione (che voi usate liberamente) +Of course this writing is interpreted by the authors as follows > ∀j:D(a,i). d(a,i,j) ∈ V -Ma se voglio usare Im per definire C, che è un subset di S, devo per -forza (almeno credo) definire un subset, ovvero dire che +If we need to use the image to define 𝐂 (a subset of S) we are obliged to +form a subset, i.e. to place a single variable `{ here | … }`. + +> Im[d(a,i)] = { y | ∃j:D(a,i). y = d(a,i,j) } -> Im[d(a,i)] = { y : S | ∃j:D(a,i). y = d(a,i,j) } +This poses no theoretical problems, since `S` is a setoid and thus equipped +with an equality. -Non ci sono problemi di sostanza, per voi S è un set, quindi ha la sua -uguaglianza..., ma quando mi chiedo se l'immagine è contenuta si -scatenano i setoidi. Ovvero Im[d(a,i)] ⊆ V diventa il seguente +Unless we difene two different images, one for stating the image is ⊆ of +something and another one to define 𝐂, we end up using always the latter. +Thus the statement `Im[d(a,i)] ⊆ V` unfolds to > ∀x:S. ( ∃j.x = d(a,i,j) ) → x ∈ V +That up to rewriting with the equation defining `x` is what we mean. The +technical problem arises when `V` is a complex construction that has to +be proved extensional (i.e. ∀x,y. x = y → x ∈ V → y ∈ V). D*) @@ -786,7 +794,10 @@ interpretation "image" 'Im a i = (image ? a i). (*D - +Thanks to our definition of image, we ca trivially a function mapping a +new axiom set to an old one and viceversa. Note that in the second +definition, when defining 𝐝, the projection of the Σ type is inlined +(constructed on the fly by `*;`) while in the paper it was named `fst`. D*) @@ -823,18 +834,23 @@ interpretation "ordinals Succ" 'oS x = (oS ? x). (*D +The dfinition of `U_x` is by recursion over the ordinal `x`. +We thus define a recursive function. The `on x` directive tells +the system on which argument the function is (structurally) recursive. + +In the `oS` case we use a local definition to name the recursive call +since it is used twice. + Note that Matita does not support notation in the left hand side of a pattern match, and thus the names of the constructors have to be spelled out verbatim. -BLA let rec. Bla let_in. - D*) nlet rec famU (A : nAx) (U : Ω^A) (x : Ord A) on x : Ω^A ≝ match x with [ oO ⇒ U - | oS y ⇒ let Un ≝ famU A U y in Un ∪ { x | ∃i.𝐈𝐦[𝐝 x i] ⊆ Un} + | oS y ⇒ let U_n ≝ famU A U y in U_n ∪ { x | ∃i.𝐈𝐦[𝐝 x i] ⊆ U_n} | oL a i f ⇒ { x | ∃j.x ∈ famU A U (f j) } ]. notation < "term 90 U \sub (term 90 x)" non associative with precedence 50 for @{ 'famU $U $x }. @@ -873,8 +889,7 @@ infinity rule. D*) -nlemma ord_subset: - ∀A:nAx.∀a:A.∀i,f,U.∀j:𝐃 a i.U⎽(f j) ⊆ U⎽(Λ f). +nlemma ord_subset: ∀A:nAx.∀a:A.∀i,f,U.∀j:𝐃 a i. U⎽(f j) ⊆ U⎽(Λ f). #A; #a; #i; #f; #U; #j; #b; #bUf; @ j; nassumption; nqed. @@ -894,9 +909,9 @@ naxiom AC : ∀A,a,i,U. (*D In the proof of infinity, we have to rewrite under the ∈ predicate. -It is clearly possible to show that U_x is an extensional set: +It is clearly possible to show that U⎽x is an extensional set: -> a=b → a ∈ U_x → b ∈ U_x +> a = b → a ∈ U⎽x → b ∈ U⎽x Anyway this proof in non trivial induction over x, that requires 𝐈 and 𝐃 to be declared as morphisms. This poses to problem, but goes out of the scope of the @@ -904,8 +919,7 @@ tutorial and we thus assume it. D*) -naxiom setoidification : - ∀A:nAx.∀a,b:A.∀x.∀U.a=b → b ∈ U⎽x → a ∈ U⎽x. +naxiom U_x_is_ext: ∀A:nAx.∀a,b:A.∀x.∀U. a = b → b ∈ U⎽x → a ∈ U⎽x. (*D @@ -913,8 +927,7 @@ The reflexivity proof is trivial, it is enough to provide the ordinal 0 as a witness, then ◃(U) reduces to U by definition, hence the conclusion. D*) -ntheorem new_coverage_reflexive: - ∀A:nAx.∀U:Ω^A.∀a. a ∈ U → a ◃ U. +ntheorem new_coverage_reflexive: ∀A:nAx.∀U:Ω^A.∀a. a ∈ U → a ◃ U. #A; #U; #a; #H; @ (0); napply H; nqed. @@ -927,6 +940,11 @@ D*) alias symbol "covers" = "new covers set". alias symbol "covers" = "new covers". alias symbol "covers" = "new covers set". +alias symbol "covers" = "new covers". +alias symbol "covers" = "new covers set". +alias symbol "covers" = "new covers". +alias symbol "covers" = "new covers set". +alias symbol "covers" = "new covers". ntheorem new_coverage_infinity: ∀A:nAx.∀U:Ω^A.∀a:A. (∃i:𝐈 a. 𝐈𝐦[𝐝 a i] ◃ U) → a ◃ U. #A; #U; #a; (** screenshot "n-cov-inf-1". *) @@ -939,7 +957,7 @@ ncut (∀j.𝐝 a i j ∈ U⎽(Λ f)); @ (Λ f+1); (** screenshot "n-cov-inf-7". *) @2; (** screenshot "n-cov-inf-8". *) @i; #x; *; #d; #Hd; (** screenshot "n-cov-inf-9". *) -napply (setoidification … Hd); napply Hf'; +napply (U_x_is_ext … Hd); napply Hf'; nqed. (*D @@ -961,7 +979,12 @@ the `#` is a standard notation for the reflexivity property of the equality. D[n-cov-inf-4] Under `H'` the axiom of choice `AC` can be eliminated, obtaining the `f` and -its property. +its property. Note that the axiom `AC` was abstracted over `A,a,i,U` before +assuming `(∀j:𝐃 a i.∃x:Ord A.𝐝 a i j ∈ U⎽x)`. Thus the term that can be eliminated +is `AC ???? H'` where the system is able to infer every `?`. Matita provides +a facility to specify a number of `?` in a compact way, i.e. `…`. The system +expand `…` first to zero, then one, then two, three and finally four question +marks, "guessing" how may of them are needed. D[n-cov-inf-5] The paper proof does now a forward reasoning step, deriving (by the ord_subset @@ -984,7 +1007,7 @@ existential, obtaining `d` (of type `𝐃 a i`) and the equation defining `x`. D[n-cov-inf-9] We just need to use the equational definition of `x` to obtain a conclusion -that can be proved with `Hf'`. We assumed that `U_x` is extensional for +that can be proved with `Hf'`. We assumed that `U⎽x` is extensional for every `x`, thus we are allowed to use `Hd` and close the proof. D*) @@ -992,7 +1015,7 @@ D*) (*D The next proof is that ◃(U) is mininal. The hardest part of the proof -it to prepare the goal for the induction. The desiderata is to prove +is to prepare the goal for the induction. The desiderata is to prove `U⎽o ⊆ V` by induction on `o`, but the conclusion of the lemma is, unfolding all definitions: @@ -1034,14 +1057,14 @@ D*) (*D -bla bla +The notion `F⎽x` is again defined by recursion over the ordinal `x`. D*) nlet rec famF (A: nAx) (F : Ω^A) (x : Ord A) on x : Ω^A ≝ match x with [ oO ⇒ F - | oS o ⇒ let Fo ≝ famF A F o in Fo ∩ { x | ∀i:𝐈 x.∃j:𝐃 x i.𝐝 x i j ∈ Fo } + | oS o ⇒ let F_o ≝ famF A F o in F_o ∩ { x | ∀i:𝐈 x.∃j:𝐃 x i.𝐝 x i j ∈ F_o } | oL a i f ⇒ { x | ∀j:𝐃 a i.x ∈ famF A F (f j) } ]. @@ -1055,11 +1078,10 @@ interpretation "new fish" 'fish a U = (mem ? (ord_fished ? U) a). (*D The proof of compatibility uses this little result, that we -factored out. +proved outside the mail proof. D*) -nlemma co_ord_subset: - ∀A:nAx.∀F:Ω^A.∀a,i.∀f:𝐃 a i → Ord A.∀j. F⎽(Λ f) ⊆ F⎽(f j). +nlemma co_ord_subset: ∀A:nAx.∀F:Ω^A.∀a,i.∀f:𝐃 a i → Ord A.∀j. F⎽(Λ f) ⊆ F⎽(f j). #A; #F; #a; #i; #f; #j; #x; #H; napply H; nqed. @@ -1068,24 +1090,23 @@ nqed. We assume the dual of the axiom of choice, as in the paper proof. D*) -naxiom AC_dual : - ∀A:nAx.∀a:A.∀i,F. (∀f:𝐃 a i → Ord A.∃x:𝐃 a i.𝐝 a i x ∈ F⎽(f x)) → ∃j:𝐃 a i.∀x:Ord A.𝐝 a i j ∈ F⎽x. +naxiom AC_dual: ∀A:nAx.∀a:A.∀i,F. + (∀f:𝐃 a i → Ord A.∃x:𝐃 a i.𝐝 a i x ∈ F⎽(f x)) → ∃j:𝐃 a i.∀x:Ord A.𝐝 a i j ∈ F⎽x. (*D -Proving the anti-reflexivity property is simce, since the +Proving the anti-reflexivity property is simple, since the assumption `a ⋉ F` states that for every ordinal `x` (and thus also 0) `a ∈ F⎽x`. If `x` is choosen to be `0`, we obtain the thesis. D*) -ntheorem new_fish_antirefl: - ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → a ∈ F. +ntheorem new_fish_antirefl: ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → a ∈ F. #A; #F; #a; #H; nlapply (H 0); #aFo; napply aFo; nqed. (*D -bar +We now prove the compatibility property for the new fish relation. D*) ntheorem new_fish_compatible: @@ -1095,19 +1116,38 @@ napply AC_dual; #f; (** screenshot "n-f-compat-2". *) nlapply (aF (Λf+1)); #aLf; (** screenshot "n-f-compat-3". *) nchange in aLf with (a ∈ F⎽(Λ f) ∧ ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ∈ F⎽(Λ f)); (** screenshot "n-f-compat-4". *) -ncut (∃j:𝐃 a i.𝐝 a i j ∈ F⎽(f j));##[ - ncases aLf; #_; #H; nlapply (H i); (** screenshot "n-f-compat-5". *) - *; #j; #Hj; @j; napply Hj;##] #aLf'; (** screenshot "n-f-compat-6". *) -napply aLf'; +ncases aLf; #_; #H; nlapply (H i); (** screenshot "n-f-compat-5". *) +*; #j; #Hj; @j; (** screenshot "n-f-compat-6". *) +napply (co_ord_subset … Hj); nqed. (*D D[n-f-compat-1] +After reducing to normal form the goal, we obseve it is exactly the conlusion of +the dual axiom of choice we just assumed. We thus apply it ad introduce the +fcuntion `f`. + D[n-f-compat-2] +The hypothesis `aF` states that `a⋉F⎽x` for every `x`, and we choose `Λf+1`. + D[n-f-compat-3] +Since F_(Λf+1) is defined by recursion and we actually have a concrete input +`Λf+1` for that recursive function, it can compute. Anyway, using the `nnormalize` +tactic would reduce too much (both the `+1` and the `Λf` steps would be prformed); +we thus explicitly give a convertible type for that hypothesis, corresponding +the computation of the `+1` step, plus the unfolding of `∩`. + D[n-f-compat-4] +We are interested in the right hand side of `aLf`, an in particular to +its intance where the generic index in `𝐈 a` is `i`. + D[n-f-compat-5] +We then eliminate the existential, obtaining `j` and its property `Hj`. We provide +the same witness + D[n-f-compat-6] +What is left to prove is exactly the `co_ord_subset` lemma we factored out +of the main proof. D*) @@ -1117,9 +1157,12 @@ The proof that `⋉(F)` is maximal is exactly the dual one of the minimality of `◃(U)`. Thus the main problem is to obtain `G ⊆ F⎽o` before doing the induction over `o`. +Note that `G` is assumed to be of type `𝛀^A`, that means an extensional +subset of `S`, while `Ω^A` means just a subset (note that the former is bold). + D*) ntheorem max_new_fished: - ∀A:nAx.∀G:qpowerclass_setoid A.∀F:Ω^A.G ⊆ F → (∀a.a ∈ G → ∀i.𝐈𝐦[𝐝 a i] ≬ G) → G ⊆ ⋉F. + ∀A:nAx.∀G:𝛀^A.∀F:Ω^A.G ⊆ F → (∀a.a ∈ G → ∀i.𝐈𝐦[𝐝 a i] ≬ G) → G ⊆ ⋉F. #A; #G; #F; #GF; #H; #b; #HbG; #o; ngeneralize in match HbG; ngeneralize in match b; nchange with (G ⊆ F⎽o); @@ -1127,13 +1170,41 @@ nelim o; ##[ napply GF; ##| #p; #IH; napply (subseteq_intersection_r … IH); #x; #Hx; #i; ncases (H … Hx i); #c; *; *; #d; #Ed; #cG; - @d; napply IH; + @d; napply IH; (** screenshot "n-f-max-1". *) + alias symbol "prop2" = "prop21". napply (. Ed^-1‡#); napply cG; ##| #a; #i; #f; #Hf; nchange with (G ⊆ { y | ∀x. y ∈ F⎽(f x) }); #b; #Hb; #d; napply (Hf d); napply Hb; ##] nqed. +(*D +D[n-f-max-1] +Here the situacion look really similar to the one of the dual proof where +we had to apply the assumption `U_x_is_ext`, but here the set is just `G` +not `F_x`. Since we assumed `G` to be extensional we can employ the facilities +Matita provides to perform rewriting in the general setting of setoids. + +The lemma `.` simply triggers the mechanism, and the given argument has to +mimick the context under which the rewriting has to happen. In that case +we want to rewrite to the left of the binary morphism `∈`. The infix notation +to represent the context of a binary morphism is `‡`. The right hand side +has to be left untouched, and the identity rewriting step is represented with +`#` (actually a reflexivity proof for the subterm identified by the context). + +We want to rewrite the left hand side using `Ed` right-to-left (the default +is left-to-right). We thus write `Ed^-1`, that is a proof that `𝐝 x i d = c`. + +The complete command is `napply (. Ed^-1‡#)` that has to be read like: + +> perform some rewritings under a binary morphism, +> on the right do nothing, +> on the left rewrite with Ed right-to-left. + +After the rewriting step the goal is exactly the `cG` assumption. + +D*) + (*D
@@ -1171,6 +1242,7 @@ of the Curry-Howard isomorphism. Where `T_rect_CProp0` is the induction principle for the inductive type `T`. + Γ ⊢ ? : Q Q ≡ P nchange with Q; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼ Γ ⊢ ? : P @@ -1187,6 +1259,17 @@ computation). Γ; H : P; Δ ⊢ ? : G + Γ; H : Q; Δ ⊢ ? : G P →* Q + nnormalize in H; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼ + Γ; H : P; Δ ⊢ ? : G + +Where `Q` is the normal form of `P` considering βδζιμν-reduction steps. + + + Γ ⊢ ? : Q P →* Q + nnormalize; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼ + Γ ⊢ ? : P + Γ ⊢ ?_2 : T → G Γ ⊢ ?_1 : T ncut T; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼