1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "sets/sets.ma".
17 nrecord category : Type[2] ≝
19 arrows: objs → objs → setoid;
20 id: ∀o:objs. arrows o o;
21 comp: ∀o1,o2,o3. unary_morphism (arrows o1 o2) (unary_morph_setoid (arrows o2 o3) (arrows o1 o3));
22 comp_assoc: ∀o1,o2,o3,o4. ∀a12,a23,a34.
23 comp o1 o3 o4 (comp o1 o2 o3 a12 a23) a34 = comp o1 o2 o4 a12 (comp o2 o3 o4 a23 a34);
24 id_neutral_left: ∀o1,o2. ∀a: arrows o1 o2. comp ??? (id o1) a = a;
25 id_neutral_right: ∀o1,o2. ∀a: arrows o1 o2. comp ??? a (id o2) = a
28 notation "hvbox(A break ⇒ B)" right associative with precedence 50 for @{ 'arrows $A $B }.
29 interpretation "arrows" 'arrows A B = (unary_morphism A B).
31 notation > "𝐈𝐝 term 90 A" non associative with precedence 90 for @{ 'id $A }.
32 notation < "mpadded width -90% (𝐈) 𝐝 \sub term 90 A" non associative with precedence 90 for @{ 'id $A }.
34 interpretation "id" 'id A = (id ? A).
36 ndefinition SETOID : category.
39 ##| napply unary_morph_setoid;
41 ##| #o1; #o2; #o3; napply mk_binary_morphism [ #f; #g; @(λx.g (f x)) ]
44 ##|##6,7: nnormalize; /2/ ]
47 unification hint 0 ≔ ;
48 R ≟ (mk_category setoid unary_morph_setoid (id SETOID) (comp SETOID)
49 (comp_assoc SETOID) (id_neutral_left SETOID)
50 (id_neutral_right SETOID))
51 (* -------------------------------------------------------------------- *) ⊢
54 unification hint 0 ≔ x,y ;
55 R ≟ (mk_category setoid unary_morph_setoid (id SETOID) (comp SETOID)
56 (comp_assoc SETOID) (id_neutral_left SETOID)
57 (id_neutral_right SETOID))
58 (* -------------------------------------------------------------------- *) ⊢
59 arrows R x y ≡ unary_morph_setoid x y.
61 unification hint 0 ≔ A,B ;
62 T ≟ (unary_morph_setoid A B)
63 (* ----------------------------------- *) ⊢
64 unary_morphism A B ≡ carr T.
68 ndefinition TYPE : setoid1.
71 alias symbol "eq" = "setoid eq".
72 napply (∃f:T1 ⇒ T2.∃g:T2 ⇒ T1. (∀x.f (g x) = x) ∧ (∀y.g (f y) = y));
73 ##| #A; @ (𝐈𝐝 A); @ (𝐈𝐝 A); @; #x; napply #;
74 ##| #A; #B; *; #f; *; #g; *; #Hfg; #Hgf; @g; @f; @; nassumption;
75 ##| #A; #B; #C; *; #f; *; #f'; *; #Hf; #Hf'; *; #g; *; #g'; *; #Hg; #Hg';
76 @; ##[ @(λx.g (f x)); #a; #b; #H; napply (.= (††H)); napply #;
77 ##| @; ##[ @(λx.f'(g' x)); #a; #b; #H; napply (.= (††H)); napply #; ##]
79 ##[ napply (.= (†(Hf …))); napply Hg;
80 ##| napply (.= (†(Hg' …))); napply Hf'; ##] ##]
83 unification hint 0 ≔ ;
84 R ≟ (mk_setoid1 setoid (eq1 TYPE))
85 (* -------------------------------------------- *) ⊢
88 nrecord unary_morphism01 (A : setoid) (B: setoid1) : Type[1] ≝
90 prop01: ∀a,a'. eq ? a a' → eq1 ? (fun01 a) (fun01 a')
93 interpretation "prop01" 'prop1 c = (prop01 ????? c).
95 nrecord nAx : Type[1] ≝ {
97 nI: unary_morphism01 nS TYPE;
98 nD: ∀a:nS. unary_morphism01 (nI a) TYPE;
99 nd: ∀a:nS. ∀i:nI a. unary_morphism (nD a i) nS
102 notation "𝐃 \sub ( ❨a,\emsp i❩ )" non associative with precedence 70 for @{ 'D $a $i }.
103 notation "𝐝 \sub ( ❨a,\emsp i,\emsp j❩ )" non associative with precedence 70 for @{ 'd $a $i $j}.
104 notation "𝐈 \sub( ❨a❩ )" non associative with precedence 70 for @{ 'I $a }.
106 notation > "𝐈 term 90 a" non associative with precedence 70 for @{ 'I $a }.
107 notation > "𝐃 term 90 a term 90 i" non associative with precedence 70 for @{ 'D $a $i }.
108 notation > "𝐝 term 90 a term 90 i term 90 j" non associative with precedence 70 for @{ 'd $a $i $j}.
110 interpretation "D" 'D a i = (nD ? a i).
111 interpretation "d" 'd a i j = (nd ? a i j).
112 interpretation "new I" 'I a = (nI ? a).
114 ndefinition image ≝ λA:nAx.λa:A.λi. { x | ∃j:𝐃 a i. x = 𝐝 a i j }.
116 nlemma elim_eq_TYPE : ∀A,B:setoid.∀P:CProp[1]. A=B → ((B ⇒ A) → P) → P.
117 #A; #B; #P; *; #f; *; #g; #_; #IH; napply IH; napply g;
120 ninductive squash (A : Type[1]) : CProp[1] ≝
121 | hide : A → squash A.
123 nrecord unary_morphism_dep (A : setoid) (T:unary_morphism01 A TYPE) : Type[1] ≝ {
124 fun_dep : ∀a:A.(T a);
125 prop_dep : ∀a,b:A. ∀H:a = b.
126 ? (prop01 … T … H) }.
129 (λf.hide ? (eq_rel ? (eq (T a)) (fun_dep a) (f (fun_dep b))))
131 ##[##2: nletin lhs ≝ (fun_dep a:?); nletin rhs ≝ (fun_dep b:?);
132 nletin patched_rhs ≝ (f rhs : ?);
133 nlapply (lhs = patched_rhs);
137 nlemma foo: ∀A:setoid.∀T:unary_morphism01 A TYPE.∀P:∀x:A.∀a:T x.CProp[0].
138 ∀x,y:A.x=y → (∃a:T x.P ? a) = (∃a:T y.P ? a).
139 #A; #T; #P; #x; #y; #H; ncases (prop01 … T … H); #f; *; #g; *; #Hf; #Hg;
145 ndefinition image_is_ext : ∀A:nAx.∀a:A.∀i:𝐈 a.𝛀^A.
146 #A; #a; #i; @ (image … i); #x; #y; #H; @;
147 ##[ *; #d; #Ex; @ d; napply (.= H^-1); nassumption;
148 ##| *; #d; #Ex; @ d; napply (.= H); nassumption; ##]
151 unification hint 0 ≔ A,a,i ;
152 R ≟ (mk_ext_powerclass ? (image A a i) (ext_prop ? (image_is_ext A a i)))
153 (* --------------------------------------------------------------- *) ⊢
154 ext_carr A R ≡ (image A a i).
156 notation > "𝐈𝐦 [𝐝 term 90 a term 90 i]" non associative with precedence 70 for @{ 'Im $a $i }.
157 notation < "mpadded width -90% (𝐈) 𝐦 [𝐝 \sub ( ❨a,\emsp i❩ )]" non associative with precedence 70 for @{ 'Im $a $i }.
159 interpretation "image" 'Im a i = (image ? a i).
161 ninductive Ord (A : nAx) : Type[0] ≝
164 | oL : ∀a:A.∀i.∀f:𝐃 a i → Ord A. Ord A.
166 notation "0" non associative with precedence 90 for @{ 'oO }.
167 notation "Λ term 90 f" non associative with precedence 50 for @{ 'oL $f }.
168 notation "x+1" non associative with precedence 50 for @{'oS $x }.
170 interpretation "ordinals Zero" 'oO = (oO ?).
171 interpretation "ordinals Lambda" 'oL f = (oL ? ? ? f).
172 interpretation "ordinals Succ" 'oS x = (oS ? x).
175 nlet rec famU (A : nAx) (U : 𝛀^A) (x : Ord A) on x : 𝛀^A ≝
177 [ oO ⇒ mk_ext_powerclass A U ?
178 | oS y ⇒ let Un ≝ famU A U y in mk_ext_powerclass A (Un ∪ { x | ∃i.𝐈𝐦[𝐝 x i] ⊆ Un}) ?
179 | oL a i f ⇒ mk_ext_powerclass A { x | ∃j.x ∈ famU A U (f j) } ? ].
180 ##[ #x; #y; #H; alias symbol "trans" = "trans1".
181 alias symbol "prop2" = "prop21".
182 napply (.= (H‡#)); napply #;
183 ##| #x; #y; #H; @; *;
184 ##[##1,3: #E; @1; ##[ napply (. (ext_prop A Un … H^-1)); ##| napply (. (ext_prop A Un … H)); ##]
186 ##|##*: *; #i; #H1; @2;
187 ##[ nlapply (†H); ##[ napply (nI A); ##| ##skip ##]
188 #W; ncases W; #f; *; #g; *; #Hf; #Hg;
189 @ (f i); #a; #Ha; napply H1;
190 ncut (𝐈𝐦[𝐝 y (f i)] = 𝐈𝐦[𝐝 x i]);
192 ##[##2: #E; napply (. (#‡E^-1)); napply Ha; ##]
195 ncut (𝐈𝐦[𝐝 y (f i)] = 𝐈𝐦[𝐝 x i]);
199 notation < "term 90 U \sub (term 90 x)" non associative with precedence 50 for @{ 'famU $U $x }.
200 notation > "U ⎽ term 90 x" non associative with precedence 50 for @{ 'famU $U $x }.
202 interpretation "famU" 'famU U x = (famU ? U x).
206 We attach as the input notation for U_x the similar `U⎽x` where underscore,
207 that is a character valid for identifier names, has been replaced by `⎽` that is
208 not. The symbol `⎽` can act as a separator, and can be typed as an alternative
209 for `_` (i.e. pressing ALT-L after `_`).
211 The notion ◃(U) has to be defined as the subset of of y
212 belonging to U_x for some x. Moreover, we have to define the notion
213 of cover between sets again, since the one defined at the beginning
214 of the tutorial works only for the old axiom set definition.
218 ndefinition ord_coverage : ∀A:nAx.∀U:Ω^A.Ω^A ≝ λA,U.{ y | ∃x:Ord A. y ∈ famU ? U x }.
220 ndefinition ord_cover_set ≝ λc:∀A:nAx.Ω^A → Ω^A.λA,C,U.
221 ∀y.y ∈ C → y ∈ c A U.
223 interpretation "coverage new cover" 'coverage U = (ord_coverage ? U).
224 interpretation "new covers set" 'covers a U = (ord_cover_set ord_coverage ? a U).
225 interpretation "new covers" 'covers a U = (mem ? (ord_coverage ? U) a).
229 Before proving that this cover relation validates the reflexivity and infinity
230 rules, we prove this little technical lemma that is used in the proof for the
236 ∀A:nAx.∀a:A.∀i,f,U.∀j:𝐃 a i.U⎽(f j) ⊆ U⎽(Λ f).
237 #A; #a; #i; #f; #U; #j; #b; #bUf; @ j; nassumption;
242 The proof of infinity uses the following form of the Axiom of choice,
243 that cannot be prove inside Matita, since the existential quantifier
244 lives in the sort of predicative propositions while the sigma in the conclusion
245 lives in the sort of data types, and thus the former cannot be eliminated
246 to provide the second.
250 naxiom AC : ∀A,a,i,U.
251 (∀j:𝐃 a i.∃x:Ord A.𝐝 a i j ∈ U⎽x) → (Σf.∀j:𝐃 a i.𝐝 a i j ∈ U⎽(f j)).
255 In the proof of infinity, we have to rewrite under the ∈ predicate.
256 It is clearly possible to show that U_x is an extensional set:
258 > a=b → a ∈ U_x → b ∈ U_x
260 Anyway this proof in non trivial induction over x, that requires 𝐈 and 𝐃 to be
261 declared as morphisms. This poses to problem, but goes out of the scope of the
262 tutorial and we thus assume it.
266 naxiom setoidification :
267 ∀A:nAx.∀a,b:A.∀x.∀U.a=b → b ∈ U⎽x → a ∈ U⎽x.
271 The reflexivity proof is trivial, it is enough to provide the ordinal 0
272 as a witness, then ◃(U) reduces to U by definition, hence the conclusion.
275 ntheorem new_coverage_reflexive:
276 ∀A:nAx.∀U:Ω^A.∀a. a ∈ U → a ◃ U.
277 #A; #U; #a; #H; @ (0); napply H;
282 We now proceed with the proof of the infinity rule.
286 alias symbol "covers" = "new covers set".
287 alias symbol "covers" = "new covers".
288 alias symbol "covers" = "new covers set".
289 alias symbol "covers" = "new covers".
290 alias symbol "covers" = "new covers set".
291 alias symbol "covers" = "new covers".
292 ntheorem new_coverage_infinity:
293 ∀A:nAx.∀U:Ω^A.∀a:A. (∃i:𝐈 a. 𝐈𝐦[𝐝 a i] ◃ U) → a ◃ U.
294 #A; #U; #a; (** screenshot "n-cov-inf-1". *)
295 *; #i; #H; nnormalize in H; (** screenshot "n-cov-inf-2". *)
296 ncut (∀y:𝐃 a i.∃x:Ord A.𝐝 a i y ∈ U⎽x); ##[ (** screenshot "n-cov-inf-3". *)
297 #z; napply H; @ z; napply #; ##] #H'; (** screenshot "n-cov-inf-4". *)
298 ncases (AC … H'); #f; #Hf; (** screenshot "n-cov-inf-5". *)
299 ncut (∀j.𝐝 a i j ∈ U⎽(Λ f));
300 ##[ #j; napply (ord_subset … f … (Hf j));##] #Hf';(** screenshot "n-cov-inf-6". *)
301 @ (Λ f+1); (** screenshot "n-cov-inf-7". *)
302 @2; (** screenshot "n-cov-inf-8". *)
303 @i; #x; *; #d; #Hd; (** screenshot "n-cov-inf-9". *)
304 napply (setoidification … Hd); napply Hf';
309 We eliminate the existential, obtaining an `i` and a proof that the
310 image of d(a,i) is covered by U. The `nnormalize` tactic computes the normal
311 form of `H`, thus expands the definition of cover between sets.
314 The paper proof considers `H` implicitly substitutes the equation assumed
315 by `H` in its conclusion. In Matita this step is not completely trivia.
316 We thus assert (`ncut`) the nicer form of `H`.
319 After introducing `z`, `H` can be applied (choosing `𝐝 a i z` as `y`).
320 What is the left to prove is that `∃j: 𝐃 a j. 𝐝 a i z = 𝐝 a i j`, that
321 becomes trivial is `j` is chosen to be `z`. In the command `napply #`,
322 the `#` is a standard notation for the reflexivity property of the equality.
325 Under `H'` the axiom of choice `AC` can be eliminated, obtaining the `f` and
329 The paper proof does now a forward reasoning step, deriving (by the ord_subset
330 lemma we proved above) `Hf'` i.e. 𝐝 a i j ∈ U⎽(Λf).
333 To prove that `a◃U` we have to exhibit the ordinal x such that `a ∈ U⎽x`.
336 The definition of `U⎽(…+1)` expands to the union of two sets, and proving
337 that `a ∈ X ∪ Y` is defined as proving that `a` is in `X` or `Y`. Applying
338 the second constructor `@2;` of the disjunction, we are left to prove that `a`
339 belongs to the right hand side.
342 We thus provide `i`, introduce the element being in the image and we are
343 left to prove that it belongs to `U_(Λf)`. In the meanwhile, since belonging
344 to the image means that there exists an object in the domain… we eliminate the
345 existential, obtaining `d` (of type `𝐃 a i`) and the equation defining `x`.
348 We just need to use the equational definition of `x` to obtain a conclusion
349 that can be proved with `Hf'`. We assumed that `U_x` is extensional for
350 every `x`, thus we are allowed to use `Hd` and close the proof.
356 The next proof is that ◃(U) is mininal. The hardest part of the proof
357 it to prepare the goal for the induction. The desiderata is to prove
358 `U⎽o ⊆ V` by induction on `o`, but the conclusion of the lemma is,
359 unfolding all definitions:
361 > ∀x. x ∈ { y | ∃o:Ord A.y ∈ U⎽o } → x ∈ V
365 nlemma new_coverage_min :
366 ∀A:nAx.∀U:Ω^A.∀V.U ⊆ V → (∀a:A.∀i.𝐈𝐦[𝐝 a i] ⊆ V → a ∈ V) → ◃U ⊆ V.
367 #A; #U; #V; #HUV; #Im;#b; (** screenshot "n-cov-min-2". *)
368 *; #o; (** screenshot "n-cov-min-3". *)
369 ngeneralize in match b; nchange with (U⎽o ⊆ V); (** screenshot "n-cov-min-4". *)
370 nelim o; (** screenshot "n-cov-min-5". *)
371 ##[ #b; #bU0; napply HUV; napply bU0;
372 ##| #p; #IH; napply subseteq_union_l; ##[ nassumption; ##]
373 #x; *; #i; #H; napply (Im ? i); napply (subseteq_trans … IH); napply H;
374 ##| #a; #i; #f; #IH; #x; *; #d; napply IH; ##]
379 After all the introductions, event the element hidden in the ⊆ definition,
380 we have to eliminate the existential quantifier, obtaining the ordinal `o`
383 What is left is almost right, but the element `b` is already in the
384 context. We thus generalize every occurrence of `b` in
385 the current goal, obtaining `∀c.c ∈ U⎽o → c ∈ V` that is `U⎽o ⊆ V`.
388 We then proceed by induction on `o` obtaining the following goals
391 All of them can be proved using simple set theoretic arguments,
392 the induction hypothesis and the assumption `Im`.
403 nlet rec famF (A: nAx) (F : Ω^A) (x : Ord A) on x : Ω^A ≝
406 | oS o ⇒ let Fo ≝ famF A F o in Fo ∩ { x | ∀i:𝐈 x.∃j:𝐃 x i.𝐝 x i j ∈ Fo }
407 | oL a i f ⇒ { x | ∀j:𝐃 a i.x ∈ famF A F (f j) }
410 interpretation "famF" 'famU U x = (famF ? U x).
412 ndefinition ord_fished : ∀A:nAx.∀F:Ω^A.Ω^A ≝ λA,F.{ y | ∀x:Ord A. y ∈ F⎽x }.
414 interpretation "fished new fish" 'fished U = (ord_fished ? U).
415 interpretation "new fish" 'fish a U = (mem ? (ord_fished ? U) a).
419 The proof of compatibility uses this little result, that we
423 nlemma co_ord_subset:
424 ∀A:nAx.∀F:Ω^A.∀a,i.∀f:𝐃 a i → Ord A.∀j. F⎽(Λ f) ⊆ F⎽(f j).
425 #A; #F; #a; #i; #f; #j; #x; #H; napply H;
430 We assume the dual of the axiom of choice, as in the paper proof.
434 ∀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.
438 Proving the anti-reflexivity property is simce, since the
439 assumption `a ⋉ F` states that for every ordinal `x` (and thus also 0)
440 `a ∈ F⎽x`. If `x` is choosen to be `0`, we obtain the thesis.
443 ntheorem new_fish_antirefl:
444 ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → a ∈ F.
445 #A; #F; #a; #H; nlapply (H 0); #aFo; napply aFo;
453 ntheorem new_fish_compatible:
454 ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ⋉ F.
455 #A; #F; #a; #aF; #i; nnormalize; (** screenshot "n-f-compat-1". *)
456 napply AC_dual; #f; (** screenshot "n-f-compat-2". *)
457 nlapply (aF (Λf+1)); #aLf; (** screenshot "n-f-compat-3". *)
459 (a ∈ F⎽(Λ f) ∧ ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ∈ F⎽(Λ f)); (** screenshot "n-f-compat-4". *)
460 ncut (∃j:𝐃 a i.𝐝 a i j ∈ F⎽(f j));##[
461 ncases aLf; #_; #H; nlapply (H i); (** screenshot "n-f-compat-5". *)
462 *; #j; #Hj; @j; napply Hj;##] #aLf'; (** screenshot "n-f-compat-6". *)
478 The proof that `⋉(F)` is maximal is exactly the dual one of the
479 minimality of `◃(U)`. Thus the main problem is to obtain `G ⊆ F⎽o`
480 before doing the induction over `o`.
483 ntheorem max_new_fished:
484 ∀A:nAx.∀G:ext_powerclass_setoid A.∀F:Ω^A.G ⊆ F → (∀a.a ∈ G → ∀i.𝐈𝐦[𝐝 a i] ≬ G) → G ⊆ ⋉F.
485 #A; #G; #F; #GF; #H; #b; #HbG; #o;
486 ngeneralize in match HbG; ngeneralize in match b;
487 nchange with (G ⊆ F⎽o);
490 ##| #p; #IH; napply (subseteq_intersection_r … IH);
491 #x; #Hx; #i; ncases (H … Hx i); #c; *; *; #d; #Ed; #cG;
493 alias symbol "prop2" = "prop21".
494 napply (. Ed^-1‡#); napply cG;
495 ##| #a; #i; #f; #Hf; nchange with (G ⊆ { y | ∀x. y ∈ F⎽(f x) });
496 #b; #Hb; #d; napply (Hf d); napply Hb;
502 <div id="appendix" class="anchor"></div>
503 Appendix: tactics explanation
504 -----------------------------
506 In this appendix we try to give a description of tactics
507 in terms of sequent calculus rules annotated with proofs.
508 The `:` separator has to be read as _is a proof of_, in the spirit
509 of the Curry-Howard isomorphism.
511 Γ ⊢ f : A1 → … → An → B Γ ⊢ ?1 : A1 … ?n : An
512 napply f; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
515 Γ ⊢ ? : F → B Γ ⊢ f : F
516 nlapply f; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
521 #x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
522 Γ ⊢ λx:T.? : ∀x:T.P(x)
525 Γ ⊢ ?_i : args_i → P(k_i args_i)
526 ncases x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
527 Γ ⊢ match x with [ k1 args1 ⇒ ?_1 | … | kn argsn ⇒ ?_n ] : P(x)
530 Γ ⊢ ?i : ∀t. P(t) → P(k_i … t …)
531 nelim x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
532 Γ ⊢ (T_rect_CProp0 ?_1 … ?_n) : P(x)
534 Where `T_rect_CProp0` is the induction principle for the
538 nchange with Q; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
541 Where the equivalence relation between types `≡` keeps into account
542 β-reduction, δ-reduction (definition unfolding), ζ-reduction (local
543 definition unfolding), ι-reduction (pattern matching simplification),
544 μ-reduction (recursive function computation) and ν-reduction (co-fixpoint
548 Γ; H : Q; Δ ⊢ ? : G Q ≡ P
549 nchange in H with Q; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
554 Γ ⊢ ?_2 : T → G Γ ⊢ ?_1 : T
555 ncut T; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
560 ngeneralize in match t; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
568 [1]: http://upsilon.cc/~zack/research/publications/notation.pdf