2 include "sets/sets.ma".
4 ndefinition binary_morph_setoid : setoid → setoid → setoid → setoid.
5 #S1; #S2; #T; @ (binary_morphism S1 S2 T); @;
6 ##[ #f; #g; napply (∀x,y. f x y = g x y);
7 ##| #f; #x; #y; napply #;
8 ##| #f; #g; #H; #x; #y; napply ((H x y)^-1);
9 ##| #f; #g; #h; #H1; #H2; #x; #y; napply (trans … (H1 …) (H2 …)); ##]
12 ndefinition unary_morph_setoid : setoid → setoid → setoid.
13 #S1; #S2; @ (unary_morphism S1 S2); @;
14 ##[ #f; #g; napply (∀x. f x = g x);
16 ##| #f; #g; #H; #x; napply ((H x)^-1);
17 ##| #f; #g; #h; #H1; #H2; #x; napply (trans … (H1 …) (H2 …)); ##]
20 nrecord category : Type[2] ≝
22 arrows: objs → objs → setoid;
23 id: ∀o:objs. arrows o o;
24 comp: ∀o1,o2,o3. binary_morphism (arrows o1 o2) (arrows o2 o3) (arrows o1 o3);
25 comp_assoc: ∀o1,o2,o3,o4. ∀a12,a23,a34.
26 comp o1 o3 o4 (comp o1 o2 o3 a12 a23) a34 = comp o1 o2 o4 a12 (comp o2 o3 o4 a23 a34);
27 id_neutral_left: ∀o1,o2. ∀a: arrows o1 o2. comp ??? (id o1) a = a;
28 id_neutral_right: ∀o1,o2. ∀a: arrows o1 o2. comp ??? a (id o2) = a
31 notation "hvbox(A break ⇒ B)" right associative with precedence 50 for @{ 'arrows $A $B }.
32 interpretation "arrows" 'arrows A B = (unary_morphism A B).
34 notation > "𝐈𝐝 term 90 A" non associative with precedence 90 for @{ 'id $A }.
35 notation < "mpadded width -90% (𝐈) 𝐝 \sub term 90 A" non associative with precedence 90 for @{ 'id $A }.
37 interpretation "id" 'id A = (id ? A).
39 ndefinition SETOID : category.
42 ##| napply unary_morph_setoid;
43 ##| #o; @ (λx.x); #a; #b; #H; napply H;
45 ##[ #f; #g; @(λx.g (f x)); #a; #b; #H; napply (.= (††H)); napply #;
46 ##| #f; #g; #f'; #g'; #H1; #H2; nwhd; #x; napply (.= (H2 (f x)));
47 napply (.= (†(H1 x))); napply #; ##]
48 ##| #o1; #o2; #o3; #o4; #f; #g; #h; nwhd; #x; napply #;
49 ##|##6,7: #o1; #o2; #f; nwhd; #x; napply #; ##]
52 unification hint 0 ≔ ;
53 R ≟ (mk_category setoid unary_morph_setoid (id SETOID) (comp SETOID)
54 (comp_assoc SETOID) (id_neutral_left SETOID)
55 (id_neutral_right SETOID))
56 (* -------------------------------------------------------------------- *) ⊢
59 unification hint 0 ≔ x,y ;
60 R ≟ (mk_category setoid unary_morph_setoid (id SETOID) (comp SETOID)
61 (comp_assoc SETOID) (id_neutral_left SETOID)
62 (id_neutral_right SETOID))
63 (* -------------------------------------------------------------------- *) ⊢
64 arrows R x y ≡ unary_morph_setoid x y.
66 unification hint 0 ≔ A,B ;
67 T ≟ (unary_morph_setoid A B)
68 (* ----------------------------------- *) ⊢
69 unary_morphism A B ≡ carr T.
72 ndefinition TYPE : setoid1.
75 alias symbol "eq" = "setoid eq".
76 napply (∃f:T1 ⇒ T2.∃g:T2 ⇒ T1. (∀x.f (g x) = x) ∧ (∀y.g (f y) = y));
77 ##| #A; @ (𝐈𝐝 A); @ (𝐈𝐝 A); @; #x; napply #;
78 ##| #A; #B; *; #f; *; #g; *; #Hfg; #Hgf; @g; @f; @; nassumption;
79 ##| #A; #B; #C; *; #f; *; #f'; *; #Hf; #Hf'; *; #g; *; #g'; *; #Hg; #Hg';
80 @; ##[ @(λx.g (f x)); #a; #b; #H; napply (.= (††H)); napply #;
81 ##| @; ##[ @(λx.f'(g' x)); #a; #b; #H; napply (.= (††H)); napply #; ##]
83 ##[ napply (.= (†(Hf …))); napply Hg;
84 ##| napply (.= (†(Hg' …))); napply Hf'; ##] ##]
87 unification hint 0 ≔ ;
88 R ≟ (mk_setoid1 setoid (eq1 TYPE))
89 (* -------------------------------------------- *) ⊢
92 nrecord unary_morphism01 (A : setoid) (B: setoid1) : Type[1] ≝
94 prop01: ∀a,a'. eq ? a a' → eq1 ? (fun01 a) (fun01 a')
97 interpretation "prop01" 'prop1 c = (prop01 ????? c).
99 nrecord nAx : Type[1] ≝ {
101 nI: unary_morphism01 nS TYPE;
102 nD: ∀a:nS. unary_morphism01 (nI a) TYPE;
103 nd: ∀a:nS. ∀i:nI a. unary_morphism (nD a i) nS
106 notation "𝐃 \sub ( ❨a,\emsp i❩ )" non associative with precedence 70 for @{ 'D $a $i }.
107 notation "𝐝 \sub ( ❨a,\emsp i,\emsp j❩ )" non associative with precedence 70 for @{ 'd $a $i $j}.
108 notation "𝐈 \sub( ❨a❩ )" non associative with precedence 70 for @{ 'I $a }.
110 notation > "𝐈 term 90 a" non associative with precedence 70 for @{ 'I $a }.
111 notation > "𝐃 term 90 a term 90 i" non associative with precedence 70 for @{ 'D $a $i }.
112 notation > "𝐝 term 90 a term 90 i term 90 j" non associative with precedence 70 for @{ 'd $a $i $j}.
114 interpretation "D" 'D a i = (nD ? a i).
115 interpretation "d" 'd a i j = (nd ? a i j).
116 interpretation "new I" 'I a = (nI ? a).
118 ndefinition image ≝ λA:nAx.λa:A.λi. { x | ∃j:𝐃 a i. x = 𝐝 a i j }.
120 nlemma elim_eq_TYPE : ∀A,B:setoid.∀P:CProp[1]. A=B → ((B ⇒ A) → P) → P.
121 #A; #B; #P; *; #f; *; #g; #_; #IH; napply IH; napply g;
124 ninductive squash (A : Type[1]) : CProp[1] ≝
125 | hide : A → squash A.
127 nrecord unary_morphism_dep (A : setoid) (T:unary_morphism01 A TYPE) : Type[1] ≝ {
128 fun_dep : ∀a:A.(T a);
129 prop_dep : ∀a,b:A. ∀H:a = b.
130 ? (prop01 … T … H) }.
133 (λf.hide ? (eq_rel ? (eq (T a)) (fun_dep a) (f (fun_dep b))))
135 ##[##2: nletin lhs ≝ (fun_dep a:?); nletin rhs ≝ (fun_dep b:?);
136 nletin patched_rhs ≝ (f rhs : ?);
137 nlapply (lhs = patched_rhs);
141 nlemma foo: ∀A:setoid.∀T:unary_morphism01 A TYPE.∀P:∀x:A.∀a:T x.CProp[0].
142 ∀x,y:A.x=y → (∃a:T x.P ? a) = (∃a:T y.P ? a).
143 #A; #T; #P; #x; #y; #H; ncases (prop01 … T … H); #f; *; #g; *; #Hf; #Hg;
148 ndefinition image_is_ext : ∀A:nAx.∀a:A.∀i:𝐈 a.𝛀^A.
149 #A; #a; #i; @ (image … i); #x; #y; #H; @;
150 ##[ *; #d; #Ex; @ d; napply (.= H^-1); nassumption;
151 ##| *; #d; #Ex; @ d; napply (.= H); nassumption; ##]
154 unification hint 0 ≔ A,a,i ;
155 R ≟ (mk_ext_powerclass ? (image A a i) (ext_prop ? (image_is_ext A a i)))
156 (* --------------------------------------------------------------- *) ⊢
157 ext_carr A R ≡ (image A a i).
159 notation > "𝐈𝐦 [𝐝 term 90 a term 90 i]" non associative with precedence 70 for @{ 'Im $a $i }.
160 notation < "mpadded width -90% (𝐈) 𝐦 [𝐝 \sub ( ❨a,\emsp i❩ )]" non associative with precedence 70 for @{ 'Im $a $i }.
162 interpretation "image" 'Im a i = (image ? a i).
164 ninductive Ord (A : nAx) : Type[0] ≝
167 | oL : ∀a:A.∀i.∀f:𝐃 a i → Ord A. Ord A.
169 notation "0" non associative with precedence 90 for @{ 'oO }.
170 notation "Λ term 90 f" non associative with precedence 50 for @{ 'oL $f }.
171 notation "x+1" non associative with precedence 50 for @{'oS $x }.
173 interpretation "ordinals Zero" 'oO = (oO ?).
174 interpretation "ordinals Lambda" 'oL f = (oL ? ? ? f).
175 interpretation "ordinals Succ" 'oS x = (oS ? x).
178 nlet rec famU (A : nAx) (U : 𝛀^A) (x : Ord A) on x : 𝛀^A ≝
180 [ oO ⇒ mk_ext_powerclass A U ?
181 | oS y ⇒ let Un ≝ famU A U y in mk_ext_powerclass A (Un ∪ { x | ∃i.𝐈𝐦[𝐝 x i] ⊆ Un}) ?
182 | oL a i f ⇒ mk_ext_powerclass A { x | ∃j.x ∈ famU A U (f j) } ? ].
183 ##[ #x; #y; #H; alias symbol "trans" = "trans1".
184 alias symbol "prop2" = "prop21".
185 napply (.= (H‡#)); napply #;
186 ##| #x; #y; #H; @; *;
187 ##[##1,3: #E; @1; ##[ napply (. (ext_prop A Un … H^-1)); ##| napply (. (ext_prop A Un … H)); ##]
189 ##|##*: *; #i; #H1; @2;
190 ##[ nlapply (†H); ##[ napply (nI A); ##| ##skip ##]
191 #W; ncases W; #f; *; #g; *; #Hf; #Hg;
192 @ (f i); #a; #Ha; napply H1;
193 ncut (𝐈𝐦[𝐝 y (f i)] = 𝐈𝐦[𝐝 x i]);
195 ##[##2: #E; alias symbol "refl" = "refl".
196 alias symbol "prop2" = "prop21 mem".
197 alias symbol "invert" = "setoid1 symmetry".
198 napply (. (#‡E^-1)); napply Ha; ##]
201 ncut (𝐈𝐦[𝐝 y (f i)] = 𝐈𝐦[𝐝 x i]);
205 notation < "term 90 U \sub (term 90 x)" non associative with precedence 50 for @{ 'famU $U $x }.
206 notation > "U ⎽ term 90 x" non associative with precedence 50 for @{ 'famU $U $x }.
208 interpretation "famU" 'famU U x = (famU ? U x).
212 We attach as the input notation for U_x the similar `U⎽x` where underscore,
213 that is a character valid for identifier names, has been replaced by `⎽` that is
214 not. The symbol `⎽` can act as a separator, and can be typed as an alternative
215 for `_` (i.e. pressing ALT-L after `_`).
217 The notion ◃(U) has to be defined as the subset of of y
218 belonging to U_x for some x. Moreover, we have to define the notion
219 of cover between sets again, since the one defined at the beginning
220 of the tutorial works only for the old axiom set definition.
224 ndefinition ord_coverage : ∀A:nAx.∀U:Ω^A.Ω^A ≝ λA,U.{ y | ∃x:Ord A. y ∈ famU ? U x }.
226 ndefinition ord_cover_set ≝ λc:∀A:nAx.Ω^A → Ω^A.λA,C,U.
227 ∀y.y ∈ C → y ∈ c A U.
229 interpretation "coverage new cover" 'coverage U = (ord_coverage ? U).
230 interpretation "new covers set" 'covers a U = (ord_cover_set ord_coverage ? a U).
231 interpretation "new covers" 'covers a U = (mem ? (ord_coverage ? U) a).
235 Before proving that this cover relation validates the reflexivity and infinity
236 rules, we prove this little technical lemma that is used in the proof for the
242 ∀A:nAx.∀a:A.∀i,f,U.∀j:𝐃 a i.U⎽(f j) ⊆ U⎽(Λ f).
243 #A; #a; #i; #f; #U; #j; #b; #bUf; @ j; nassumption;
248 The proof of infinity uses the following form of the Axiom of choice,
249 that cannot be prove inside Matita, since the existential quantifier
250 lives in the sort of predicative propositions while the sigma in the conclusion
251 lives in the sort of data types, and thus the former cannot be eliminated
252 to provide the second.
256 naxiom AC : ∀A,a,i,U.
257 (∀j:𝐃 a i.∃x:Ord A.𝐝 a i j ∈ U⎽x) → (Σf.∀j:𝐃 a i.𝐝 a i j ∈ U⎽(f j)).
261 In the proof of infinity, we have to rewrite under the ∈ predicate.
262 It is clearly possible to show that U_x is an extensional set:
264 > a=b → a ∈ U_x → b ∈ U_x
266 Anyway this proof in non trivial induction over x, that requires 𝐈 and 𝐃 to be
267 declared as morphisms. This poses to problem, but goes out of the scope of the
268 tutorial and we thus assume it.
272 naxiom setoidification :
273 ∀A:nAx.∀a,b:A.∀x.∀U.a=b → b ∈ U⎽x → a ∈ U⎽x.
277 The reflexivity proof is trivial, it is enough to provide the ordinal 0
278 as a witness, then ◃(U) reduces to U by definition, hence the conclusion.
281 ntheorem new_coverage_reflexive:
282 ∀A:nAx.∀U:Ω^A.∀a. a ∈ U → a ◃ U.
283 #A; #U; #a; #H; @ (0); napply H;
288 We now proceed with the proof of the infinity rule.
292 alias symbol "covers" = "new covers set".
293 alias symbol "covers" = "new covers".
294 alias symbol "covers" = "new covers set".
295 alias symbol "covers" = "new covers".
296 alias symbol "covers" = "new covers set".
297 alias symbol "covers" = "new covers".
298 ntheorem new_coverage_infinity:
299 ∀A:nAx.∀U:Ω^A.∀a:A. (∃i:𝐈 a. 𝐈𝐦[𝐝 a i] ◃ U) → a ◃ U.
300 #A; #U; #a; (** screenshot "n-cov-inf-1". *)
301 *; #i; #H; nnormalize in H; (** screenshot "n-cov-inf-2". *)
302 ncut (∀y:𝐃 a i.∃x:Ord A.𝐝 a i y ∈ U⎽x); ##[ (** screenshot "n-cov-inf-3". *)
303 #z; napply H; @ z; napply #; ##] #H'; (** screenshot "n-cov-inf-4". *)
304 ncases (AC … H'); #f; #Hf; (** screenshot "n-cov-inf-5". *)
305 ncut (∀j.𝐝 a i j ∈ U⎽(Λ f));
306 ##[ #j; napply (ord_subset … f … (Hf j));##] #Hf';(** screenshot "n-cov-inf-6". *)
307 @ (Λ f+1); (** screenshot "n-cov-inf-7". *)
308 @2; (** screenshot "n-cov-inf-8". *)
309 @i; #x; *; #d; #Hd; (** screenshot "n-cov-inf-9". *)
310 napply (setoidification … Hd); napply Hf';
315 We eliminate the existential, obtaining an `i` and a proof that the
316 image of d(a,i) is covered by U. The `nnormalize` tactic computes the normal
317 form of `H`, thus expands the definition of cover between sets.
320 The paper proof considers `H` implicitly substitutes the equation assumed
321 by `H` in its conclusion. In Matita this step is not completely trivia.
322 We thus assert (`ncut`) the nicer form of `H`.
325 After introducing `z`, `H` can be applied (choosing `𝐝 a i z` as `y`).
326 What is the left to prove is that `∃j: 𝐃 a j. 𝐝 a i z = 𝐝 a i j`, that
327 becomes trivial is `j` is chosen to be `z`. In the command `napply #`,
328 the `#` is a standard notation for the reflexivity property of the equality.
331 Under `H'` the axiom of choice `AC` can be eliminated, obtaining the `f` and
335 The paper proof does now a forward reasoning step, deriving (by the ord_subset
336 lemma we proved above) `Hf'` i.e. 𝐝 a i j ∈ U⎽(Λf).
339 To prove that `a◃U` we have to exhibit the ordinal x such that `a ∈ U⎽x`.
342 The definition of `U⎽(…+1)` expands to the union of two sets, and proving
343 that `a ∈ X ∪ Y` is defined as proving that `a` is in `X` or `Y`. Applying
344 the second constructor `@2;` of the disjunction, we are left to prove that `a`
345 belongs to the right hand side.
348 We thus provide `i`, introduce the element being in the image and we are
349 left to prove that it belongs to `U_(Λf)`. In the meanwhile, since belonging
350 to the image means that there exists an object in the domain… we eliminate the
351 existential, obtaining `d` (of type `𝐃 a i`) and the equation defining `x`.
354 We just need to use the equational definition of `x` to obtain a conclusion
355 that can be proved with `Hf'`. We assumed that `U_x` is extensional for
356 every `x`, thus we are allowed to use `Hd` and close the proof.
362 The next proof is that ◃(U) is mininal. The hardest part of the proof
363 it to prepare the goal for the induction. The desiderata is to prove
364 `U⎽o ⊆ V` by induction on `o`, but the conclusion of the lemma is,
365 unfolding all definitions:
367 > ∀x. x ∈ { y | ∃o:Ord A.y ∈ U⎽o } → x ∈ V
371 nlemma new_coverage_min :
372 ∀A:nAx.∀U:Ω^A.∀V.U ⊆ V → (∀a:A.∀i.𝐈𝐦[𝐝 a i] ⊆ V → a ∈ V) → ◃U ⊆ V.
373 #A; #U; #V; #HUV; #Im;#b; (** screenshot "n-cov-min-2". *)
374 *; #o; (** screenshot "n-cov-min-3". *)
375 ngeneralize in match b; nchange with (U⎽o ⊆ V); (** screenshot "n-cov-min-4". *)
376 nelim o; (** screenshot "n-cov-min-5". *)
377 ##[ #b; #bU0; napply HUV; napply bU0;
378 ##| #p; #IH; napply subseteq_union_l; ##[ nassumption; ##]
379 #x; *; #i; #H; napply (Im ? i); napply (subseteq_trans … IH); napply H;
380 ##| #a; #i; #f; #IH; #x; *; #d; napply IH; ##]
385 After all the introductions, event the element hidden in the ⊆ definition,
386 we have to eliminate the existential quantifier, obtaining the ordinal `o`
389 What is left is almost right, but the element `b` is already in the
390 context. We thus generalize every occurrence of `b` in
391 the current goal, obtaining `∀c.c ∈ U⎽o → c ∈ V` that is `U⎽o ⊆ V`.
394 We then proceed by induction on `o` obtaining the following goals
397 All of them can be proved using simple set theoretic arguments,
398 the induction hypothesis and the assumption `Im`.
409 nlet rec famF (A: nAx) (F : Ω^A) (x : Ord A) on x : Ω^A ≝
412 | oS o ⇒ let Fo ≝ famF A F o in Fo ∩ { x | ∀i:𝐈 x.∃j:𝐃 x i.𝐝 x i j ∈ Fo }
413 | oL a i f ⇒ { x | ∀j:𝐃 a i.x ∈ famF A F (f j) }
416 interpretation "famF" 'famU U x = (famF ? U x).
418 ndefinition ord_fished : ∀A:nAx.∀F:Ω^A.Ω^A ≝ λA,F.{ y | ∀x:Ord A. y ∈ F⎽x }.
420 interpretation "fished new fish" 'fished U = (ord_fished ? U).
421 interpretation "new fish" 'fish a U = (mem ? (ord_fished ? U) a).
425 The proof of compatibility uses this little result, that we
429 nlemma co_ord_subset:
430 ∀A:nAx.∀F:Ω^A.∀a,i.∀f:𝐃 a i → Ord A.∀j. F⎽(Λ f) ⊆ F⎽(f j).
431 #A; #F; #a; #i; #f; #j; #x; #H; napply H;
436 We assume the dual of the axiom of choice, as in the paper proof.
440 ∀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.
444 Proving the anti-reflexivity property is simce, since the
445 assumption `a ⋉ F` states that for every ordinal `x` (and thus also 0)
446 `a ∈ F⎽x`. If `x` is choosen to be `0`, we obtain the thesis.
449 ntheorem new_fish_antirefl:
450 ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → a ∈ F.
451 #A; #F; #a; #H; nlapply (H 0); #aFo; napply aFo;
459 ntheorem new_fish_compatible:
460 ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ⋉ F.
461 #A; #F; #a; #aF; #i; nnormalize; (** screenshot "n-f-compat-1". *)
462 napply AC_dual; #f; (** screenshot "n-f-compat-2". *)
463 nlapply (aF (Λf+1)); #aLf; (** screenshot "n-f-compat-3". *)
465 (a ∈ F⎽(Λ f) ∧ ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ∈ F⎽(Λ f)); (** screenshot "n-f-compat-4". *)
466 ncut (∃j:𝐃 a i.𝐝 a i j ∈ F⎽(f j));##[
467 ncases aLf; #_; #H; nlapply (H i); (** screenshot "n-f-compat-5". *)
468 *; #j; #Hj; @j; napply Hj;##] #aLf'; (** screenshot "n-f-compat-6". *)
484 The proof that `⋉(F)` is maximal is exactly the dual one of the
485 minimality of `◃(U)`. Thus the main problem is to obtain `G ⊆ F⎽o`
486 before doing the induction over `o`.
489 ntheorem max_new_fished:
490 ∀A:nAx.∀G:ext_powerclass_setoid A.∀F:Ω^A.G ⊆ F → (∀a.a ∈ G → ∀i.𝐈𝐦[𝐝 a i] ≬ G) → G ⊆ ⋉F.
491 #A; #G; #F; #GF; #H; #b; #HbG; #o;
492 ngeneralize in match HbG; ngeneralize in match b;
493 nchange with (G ⊆ F⎽o);
496 ##| #p; #IH; napply (subseteq_intersection_r … IH);
497 #x; #Hx; #i; ncases (H … Hx i); #c; *; *; #d; #Ed; #cG;
499 alias symbol "prop2" = "prop21".
500 napply (. Ed^-1‡#); napply cG;
501 ##| #a; #i; #f; #Hf; nchange with (G ⊆ { y | ∀x. y ∈ F⎽(f x) });
502 #b; #Hb; #d; napply (Hf d); napply Hb;
508 <div id="appendix" class="anchor"></div>
509 Appendix: tactics explanation
510 -----------------------------
512 In this appendix we try to give a description of tactics
513 in terms of sequent calculus rules annotated with proofs.
514 The `:` separator has to be read as _is a proof of_, in the spirit
515 of the Curry-Howard isomorphism.
517 Γ ⊢ f : A1 → … → An → B Γ ⊢ ?1 : A1 … ?n : An
518 napply f; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
521 Γ ⊢ ? : F → B Γ ⊢ f : F
522 nlapply f; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
527 #x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
528 Γ ⊢ λx:T.? : ∀x:T.P(x)
531 Γ ⊢ ?_i : args_i → P(k_i args_i)
532 ncases x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
533 Γ ⊢ match x with [ k1 args1 ⇒ ?_1 | … | kn argsn ⇒ ?_n ] : P(x)
536 Γ ⊢ ?i : ∀t. P(t) → P(k_i … t …)
537 nelim x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
538 Γ ⊢ (T_rect_CProp0 ?_1 … ?_n) : P(x)
540 Where `T_rect_CProp0` is the induction principle for the
544 nchange with Q; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
547 Where the equivalence relation between types `≡` keeps into account
548 β-reduction, δ-reduction (definition unfolding), ζ-reduction (local
549 definition unfolding), ι-reduction (pattern matching simplification),
550 μ-reduction (recursive function computation) and ν-reduction (co-fixpoint
554 Γ; H : Q; Δ ⊢ ? : G Q ≡ P
555 nchange in H with Q; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
560 Γ ⊢ ?_2 : T → G Γ ⊢ ?_1 : T
561 ncut T; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
566 ngeneralize in match t; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
574 [1]: http://upsilon.cc/~zack/research/publications/notation.pdf