helm/software/matita/nlibrary/topology/igft.ma

   1 (*DOCBEGIN
   2
   3 Matita Tutorial: inductively generated formal topologies
   4 ========================================================
   5
   6 This is a not so short introduction to Matita, based on
   7 the formalization of the paper
   8
   9 > Between formal topology and game theory: an
  10 > explicit solution for the conditions for an
  11 > inductive generation of formal topologies
  12
  13 by S.Berardi and S. Valentini.
  14
  15 Orientering
  16 -----------
  17
  18 TODO
  19
  20 buttons, PG-interaction-model, sequent window, script window
  21
  22 The library, inclusion of `sets/sets.ma`, notation defined: Ω^A.
  23 Symbols (see menu: View ▹ TeX/UTF-8 Table):
  24
  25 - ∀ `\Forall`
  26 - λ `\lambda`
  27 - ≝ `\def`
  28 - → `->`
  29
  30 Virtuals, ALT-L, for example `I` changes into `𝕀`, finally `𝐈`.
  31
  32 The standard library and the `include` command
  33 ----------------------------------------------
  34
  35 Some basic notions, like subset, membership, intersection and union
  36 are part of the standard library of Matita.
  37
  38 These notions come with
  39 some notation attached to them:
  40
  41 - A ∪ B `A \cup B`
  42 - A ∩ B `A \cap B`
  43 - x ∈ A `x \in A`
  44 - Ω^A, that is the type of the subsets of A, `\Omega ^ A`
  45
  46 The `include` command tells Matita to load a part of the library,
  47 in particular the part that we will use can be loaded as follows:
  48
  49 DOCEND*)
  50
  51 include "sets/sets.ma".
  52
  53 (*HIDE*)
  54 (* move away *)
  55 nlemma subseteq_intersection_l: ∀A.∀U,V,W:Ω^A.U ⊆ W ∨ V ⊆ W → U ∩ V ⊆ W.
  56 #A; #U; #V; #W; *; #H; #x; *; #xU; #xV; napply H; nassumption;
  57 nqed.
  58
  59 nlemma subseteq_union_l: ∀A.∀U,V,W:Ω^A.U ⊆ W → V ⊆ W → U ∪ V ⊆ W.
  60 #A; #U; #V; #W; #H; #H1; #x; *; #Hx; ##[ napply H; ##| napply H1; ##] nassumption;
  61 nqed.
  62
  63 nlemma subseteq_intersection_r: ∀A.∀U,V,W:Ω^A.W ⊆ U → W ⊆ V → W ⊆ U ∩ V.
  64 #A; #U; #V; #W; #H1; #H2; #x; #Hx; @; ##[ napply H1; ##| napply H2; ##] nassumption;
  65 nqed.
  66 (*UNHIDE*)
  67
  68 (*DOCBEGIN
  69
  70 Some basic results that we will use are also part of the sets library:
  71
  72 - subseteq\_union\_l: ∀A.∀U,V,W:Ω^A.U ⊆ W → V ⊆ W → U ∪ V ⊆ W
  73 - subseteq\_intersection\_r: ∀A.∀U,V,W:Ω^A.W ⊆ U → W ⊆ V → W ⊆ U ∩ V
  74
  75 Defining Axiom set
  76 ------------------
  77
  78 records, ...
  79
  80 DOCEND*)
  81
  82 nrecord Ax : Type[1] ≝ {
  83   S:> setoid;
  84   I: S → Type[0];
  85   C: ∀a:S. I a → Ω ^ S
  86 }.
  87
  88 (*DOCBEGIN
  89
  90 TODO: coercion S.
  91
  92 Something that is not still satisfactory, in that the dependent type
  93 of `I` and `C` are abstracted over the Axiom set. To obtain the
  94 precise type of a term, you can use the `ncheck` command as follows.
  95
  96 DOCEND*)
  97
  98 (* ncheck I. *)
  99 (* ncheck C. *)
 100
 101 (*DOCBEGIN
 102
 103 One would like to write `I a` and not `I A a` under a context where
 104 `A` is an axiom set and `a` has type `S A` (or thanks to the coercion
 105 mecanism simply `A`). Matita performs type inference, thus writing
 106 `I ? a` is enough, since the second argument of `I` is typed by the
 107 first one, the first one can be inferred just computing the type of `a`.
 108
 109 DOCEND*)
 110
 111 (* ncheck (∀A:Ax.∀a:A.I ? a). *)
 112
 113 (*DOCBEGIN
 114
 115 This is still not completely satisfactory, and to fix this minor issue
 116 we have to introduce the notational support built in Matita.
 117
 118 Notation for I and C
 119 --------------------
 120
 121 Matita is quipped qith a quite complex notational support,
 122 allowing the user to define and use mathematical notations
 123 ([From Notation to Semantics: There and Back Again][1]).
 124
 125 Since notations are usually ambiguous (e.g. the frequent overloading of
 126 symbols) Matita distinguishes between the term level, the
 127 content level, and the presentation level.
 128
 129 The mapping between the presentation level (i.e. what is typed on the
 130 keyboard and what is displayed in the sequent window) and the content
 131 level is defined with the `notation` command. When followed by
 132 `>`, it defines an input (only) notation.
 133
 134 DOCEND*)
 135
 136 notation > "𝐈 term 90 a" non associative with precedence 70 for @{ 'I $a }.
 137 notation > "𝐂 term 90 a term 90 i" non associative with precedence 70 for @{ 'C $a $i }.
 138
 139 (*DOCBEGIN
 140
 141 The forst notation defines the writing `𝐈 a` where `a` is a generic
 142 term of precedence 90, the maximum one. This high precedence forces
 143 parentheses around any term of a lower precedence. For example `𝐈 x`
 144 would be accepted, since identifiers have precedence 90, but
 145 `𝐈 f x` would be interpreted as `(𝐈 f) x`. In the latter case, parentheses
 146 have to be put around `f x`, thus the accepted writing would be `𝐈 (f x)`.
 147
 148 To obtain the `𝐈` is enough to type `I` and then cycle between its
 149 similar symbols with ALT-L. The same for `𝐂`. Notationa cannot use
 150 regular letters or the round parentheses, thus their variants (like the
 151 bold ones) have to be used.
 152
 153 The first notation associates `𝐈 a` with `'I $a` where `'I` is a
 154 new content element to which a term `$a` is passed.
 155
 156 Content elements have to be interpreted, and possibly multiple,
 157 incompatible, interpretations can be defined.
 158
 159 DOCEND*)
 160
 161 interpretation "I" 'I a = (I ? a).
 162 interpretation "C" 'C a i = (C ? a i).
 163
 164 (*DOCBEGIN
 165
 166 The `interpretation` command allows to define the mapping between
 167 the content level and the terms level. Here we associate the `I` and
 168 `C` projections of the Axiom set record, where the Axiom set is an implicit
 169 argument `?` to be inferred by the system.
 170
 171 Interpretation are bi-directional, thus when displaying a term like
 172 `C _ a i`, the system looks for a presentation for the content element
 173 `'C a i`.
 174
 175 DOCEND*)
 176
 177 notation < "𝐈  \sub( ❨a❩ )" non associative with precedence 70 for @{ 'I $a }.
 178 notation < "𝐂 \sub( ❨a,\emsp i❩ )" non associative with precedence 70 for @{ 'C $a $i }.
 179
 180 (*DOCBEGIN
 181
 182 For output purposes we can define more complex notations, for example
 183 we can put bold parenteses around the arguments of `𝐈` and `𝐂`, decreasing
 184 the size of the arguments and lowering their baseline (i.e. putting them
 185 as subscript), separating them with a comma followed by a little space.
 186
 187 The first (technical) definition
 188 --------------------------------
 189
 190
 191
 192 DOCEND*)
 193
 194 ndefinition cover_set :
 195   ∀c: ∀A:Ax.Ω^A → A → CProp[0]. ∀A:Ax.∀C,U:Ω^A. CProp[0]
 196 ≝
 197   λc: ∀A:Ax.Ω^A → A → CProp[0]. λA,C,U.∀y.y ∈ C → c A U y.
 198
 199 ndefinition cover_set_interactive :
 200   ∀c: ∀A:Ax.Ω^A → A → CProp[0]. ∀A:Ax.∀C,U:Ω^A. CProp[0].
 201 #cover; #A; #C; #U; napply (∀y:A.y ∈ C → ?); napply cover;
 202 ##[ napply A;
 203 ##| napply U;
 204 ##| napply y;
 205 ##]
 206 nqed.
 207
 208 (* a \ltri b *)
 209 notation "hvbox(a break ◃ b)" non associative with precedence 45
 210 for @{ 'covers $a $b }.
 211
 212 interpretation "covers set temp" 'covers C U = (cover_set ?? C U).
 213
 214 ninductive cover (A : Ax) (U : Ω^A) : A → CProp[0] ≝
 215 | creflexivity : ∀a:A. a ∈ U → cover ? U a
 216 | cinfinity    : ∀a:A.∀i:𝐈 a. 𝐂 a i ◃ U → cover ? U a.
 217 napply cover;
 218 nqed.
 219
 220 interpretation "covers" 'covers a U = (cover ? U a).
 221 (* interpretation "covers set" 'covers a U = (cover_set cover ? a U). *)
 222
 223 ndefinition fish_set ≝ λf:∀A:Ax.Ω^A → A → CProp[0].
 224  λA,U,V.
 225   ∃a.a ∈ V ∧ f A U a.
 226
 227 (* a \ltimes b *)
 228 notation "hvbox(a break ⋉ b)" non associative with precedence 45
 229 for @{ 'fish $a $b }.
 230
 231 interpretation "fish set temp" 'fish A U = (fish_set ?? U A).
 232
 233 ncoinductive fish (A : Ax) (F : Ω^A) : A → CProp[0] ≝
 234 | cfish : ∀a. a ∈ F → (∀i:𝐈 a .𝐂  a i ⋉ F) → fish A F a.
 235 napply fish;
 236 nqed.
 237
 238 interpretation "fish set" 'fish A U = (fish_set fish ? U A).
 239 interpretation "fish" 'fish a U = (fish ? U a).
 240
 241 nlet corec fish_rec (A:Ax) (U: Ω^A)
 242  (P: Ω^A) (H1: P ⊆ U)
 243   (H2: ∀a:A. a ∈ P → ∀j: 𝐈 a. 𝐂 a j ≬ P):
 244    ∀a:A. ∀p: a ∈ P. a ⋉ U ≝ ?.
 245 #a; #p; napply cfish; (** screenshot "def-fish-rec". *)
 246 ##[ napply H1; napply p;
 247 ##| #i; ncases (H2 a p i); #x; *; #xC; #xP; @; ##[napply x]
 248     @; ##[ napply xC ] napply (fish_rec ? U P); nassumption;
 249 ##]
 250 nqed.
 251
 252 notation "◃U" non associative with precedence 55
 253 for @{ 'coverage $U }.
 254
 255 ndefinition coverage : ∀A:Ax.∀U:Ω^A.Ω^A ≝ λA,U.{ a | a ◃ U }.
 256
 257 interpretation "coverage cover" 'coverage U = (coverage ? U).
 258
 259 ndefinition cover_equation : ∀A:Ax.∀U,X:Ω^A.CProp[0] ≝  λA,U,X.
 260   ∀a.a ∈ X ↔ (a ∈ U ∨ ∃i:𝐈 a.∀y.y ∈ 𝐂 a i → y ∈ X).
 261
 262 ntheorem coverage_cover_equation : ∀A,U. cover_equation A U (◃U).
 263 #A; #U; #a; @; #H;
 264 ##[ nelim H; #b; (* manca clear *)
 265     ##[ #bU; @1; nassumption;
 266     ##| #i; #CaiU; #IH; @2; @ i; #c; #cCbi; ncases (IH ? cCbi);
 267         ##[ #E; @; napply E;
 268         ##| #_; napply CaiU; nassumption; ##] ##]
 269 ##| ncases H; ##[ #E; @; nassumption]
 270     *; #j; #Hj; @2 j; #w; #wC; napply Hj; nassumption;
 271 ##]
 272 nqed.
 273
 274 ntheorem coverage_min_cover_equation :
 275   ∀A,U,W. cover_equation A U W → ◃U ⊆ W.
 276 #A; #U; #W; #H; #a; #aU; nelim aU; #b;
 277 ##[ #bU; ncases (H b); #_; #H1; napply H1; @1; nassumption;
 278 ##| #i; #CbiU; #IH; ncases (H b); #_; #H1; napply H1; @2; @i; napply IH;
 279 ##]
 280 nqed.
 281
 282 notation "⋉F" non associative with precedence 55
 283 for @{ 'fished $F }.
 284
 285 ndefinition fished : ∀A:Ax.∀F:Ω^A.Ω^A ≝ λA,F.{ a | a ⋉ F }.
 286
 287 interpretation "fished fish" 'fished F = (fished ? F).
 288
 289 ndefinition fish_equation : ∀A:Ax.∀F,X:Ω^A.CProp[0] ≝ λA,F,X.
 290   ∀a. a ∈ X ↔ a ∈ F ∧ ∀i:𝐈 a.∃y.y ∈ 𝐂 a i ∧ y ∈ X.
 291
 292 ntheorem fised_fish_equation : ∀A,F. fish_equation A F (⋉F).
 293 #A; #F; #a; @; (* bug, fare case sotto diverso da farlo sopra *) #H; ncases H;
 294 ##[ #b; #bF; #H2; @ bF; #i; ncases (H2 i); #c; *; #cC; #cF; @c; @ cC;
 295     napply cF;
 296 ##| #aF; #H1; @ aF; napply H1;
 297 ##]
 298 nqed.
 299
 300 ntheorem fised_max_fish_equation : ∀A,F,G. fish_equation A F G → G ⊆ ⋉F.
 301 #A; #F; #G; #H; #a; #aG; napply (fish_rec … aG);
 302 #b; ncases (H b); #H1; #_; #bG; ncases (H1 bG); #E1; #E2; nassumption;
 303 nqed.
 304
 305 nrecord nAx : Type[2] ≝ {
 306   nS:> setoid; (*Type[0];*)
 307   nI: nS → Type[0];
 308   nD: ∀a:nS. nI a → Type[0];
 309   nd: ∀a:nS. ∀i:nI a. nD a i → nS
 310 }.
 311
 312 (*
 313 TYPE f A → B, g : B → A, f ∘ g = id, g ∘ g = id.
 314
 315 a = b → I a = I b
 316 *)
 317
 318 notation "𝐃 \sub ( ❨a,\emsp i❩ )" non associative with precedence 70 for @{ 'D $a $i }.
 319 notation "𝐝 \sub ( ❨a,\emsp i,\emsp j❩ )" non associative with precedence 70 for @{ 'd $a $i $j}.
 320
 321 notation > "𝐃 term 90 a term 90 i" non associative with precedence 70 for @{ 'D $a $i }.
 322 notation > "𝐝 term 90 a term 90 i term 90 j" non associative with precedence 70 for @{ 'd $a $i $j}.
 323
 324 interpretation "D" 'D a i = (nD ? a i).
 325 interpretation "d" 'd a i j = (nd ? a i j).
 326 interpretation "new I" 'I a = (nI ? a).
 327
 328 ndefinition image ≝ λA:nAx.λa:A.λi. { x | ∃j:𝐃 a i. x = 𝐝 a i j }.
 329
 330 notation > "𝐈𝐦  [𝐝 term 90 a term 90 i]" non associative with precedence 70 for @{ 'Im $a $i }.
 331 notation "𝐈𝐦  [𝐝 \sub ( ❨a,\emsp i❩ )]" non associative with precedence 70 for @{ 'Im $a $i }.
 332
 333 interpretation "image" 'Im a i = (image ? a i).
 334
 335 ndefinition Ax_of_nAx : nAx → Ax.
 336 #A; @ A (nI ?); #a; #i; napply (𝐈𝐦 [𝐝 a i]);
 337 nqed.
 338
 339 ninductive sigma (A : Type[0]) (P : A → CProp[0]) : Type[0] ≝
 340  sig_intro : ∀x:A.P x → sigma A P.
 341
 342 interpretation "sigma" 'sigma \eta.p = (sigma ? p).
 343
 344 ndefinition nAx_of_Ax : Ax → nAx.
 345 #A; @ A (I ?);
 346 ##[ #a; #i; napply (Σx:A.x ∈ 𝐂 a i);
 347 ##| #a; #i; *; #x; #_; napply x;
 348 ##]
 349 nqed.
 350
 351 ninductive Ord (A : nAx) : Type[0] ≝
 352  | oO : Ord A
 353  | oS : Ord A → Ord A
 354  | oL : ∀a:A.∀i.∀f:𝐃 a i → Ord A. Ord A.
 355
 356 notation "Λ term 90 f" non associative with precedence 50 for @{ 'oL $f }.
 357 notation "x+1" non associative with precedence 50 for @{'oS $x }.
 358
 359 interpretation "ordinals Lambda" 'oL f = (oL ? ? ? f).
 360 interpretation "ordinals Succ" 'oS x = (oS ? x).
 361
 362 nlet rec famU (A : nAx) (U : Ω^A) (x : Ord A) on x : Ω^A ≝
 363   match x with
 364   [ oO ⇒ U
 365   | oS y ⇒ let Un ≝ famU A U y in Un ∪ { x | ∃i.𝐈𝐦[𝐝 x i] ⊆ Un}
 366   | oL a i f ⇒ { x | ∃j.x ∈ famU A U (f j) } ].
 367
 368 notation < "term 90 U \sub (term 90 x)" non associative with precedence 50 for @{ 'famU $U $x }.
 369 notation > "U ⎽ term 90 x" non associative with precedence 50 for @{ 'famU $U $x }.
 370
 371 interpretation "famU" 'famU U x = (famU ? U x).
 372
 373 ndefinition ord_coverage : ∀A:nAx.∀U:Ω^A.Ω^A ≝ λA,U.{ y | ∃x:Ord A. y ∈ famU ? U x }.
 374
 375 ndefinition ord_cover_set ≝ λc:∀A:nAx.Ω^A → Ω^A.λA,C,U.
 376   ∀y.y ∈ C → y ∈ c A U.
 377
 378 interpretation "coverage new cover" 'coverage U = (ord_coverage ? U).
 379 interpretation "new covers set" 'covers a U = (ord_cover_set ord_coverage ? a U).
 380 interpretation "new covers" 'covers a U = (mem ? (ord_coverage ? U) a).
 381
 382 ntheorem new_coverage_reflexive:
 383   ∀A:nAx.∀U:Ω^A.∀a. a ∈ U → a ◃ U.
 384 #A; #U; #a; #H; @ (oO A); napply H;
 385 nqed.
 386
 387 nlemma ord_subset:
 388   ∀A:nAx.∀a:A.∀i,f,U.∀j:𝐃 a i.U⎽(f j) ⊆ U⎽(Λ f).
 389 #A; #a; #i; #f; #U; #j; #b; #bUf; @ j; nassumption;
 390 nqed.
 391
 392 naxiom AC : ∀A,a,i,U.(∀j:𝐃 a i.∃x:Ord A.𝐝 a i j ∈ U⎽x) → (Σf.∀j:𝐃 a i.𝐝 a i j ∈ U⎽(f j)).
 393
 394 naxiom setoidification :
 395   ∀A:nAx.∀a,b:A.∀U.a=b → b ∈ U → a ∈ U.
 396
 397 (*DOCBEGIN
 398
 399 Bla Bla,
 400
 401 <div id="figure1" class="img" ><img src="figure1.png"/>foo</div>
 402
 403 DOCEND*)
 404
 405 alias symbol "covers" = "new covers".
 406 alias symbol "covers" = "new covers set".
 407 alias symbol "covers" = "new covers".
 408 alias symbol "covers" = "new covers set".
 409 alias symbol "covers" = "new covers".
 410 alias symbol "covers" = "new covers set".
 411 alias symbol "covers" = "new covers".
 412 alias symbol "covers" = "new covers set".
 413 alias symbol "covers" = "new covers".
 414 ntheorem new_coverage_infinity:
 415   ∀A:nAx.∀U:Ω^A.∀a:A. (∃i:𝐈 a. 𝐈𝐦[𝐝 a i] ◃ U) → a ◃ U.
 416 #A; #U; #a;(** screenshot "figure1". *)
 417 *; #i; #H; nnormalize in H;
 418 ncut (∀y:𝐃 a i.∃x:Ord A.𝐝 a i y ∈ U⎽x); ##[
 419   #y; napply H; @ y; napply #; ##] #H';
 420 ncases (AC … H'); #f; #Hf;
 421 ncut (∀j.𝐝 a i j ∈ U⎽(Λ f));
 422   ##[ #j; napply (ord_subset … f … (Hf j));##] #Hf';
 423 @ ((Λ f)+1); @2; nwhd; @i; #x; *; #d; #Hd;
 424 napply (setoidification … Hd); napply Hf';
 425 nqed.
 426
 427 nlemma new_coverage_min :
 428   ∀A:nAx.∀U:qpowerclass A.∀V.U ⊆ V → (∀a:A.∀i.𝐈𝐦[𝐝 a i] ⊆ V → a ∈ V) → ◃(pc ? U) ⊆ V.
 429 #A; #U; #V; #HUV; #Im;  #b; *; #o; ngeneralize in match b; nchange with ((pc ? U)⎽o ⊆ V);
 430 nelim o;
 431 ##[ #b; #bU0; napply HUV; napply bU0;
 432 ##| #p; #IH; napply subseteq_union_l; ##[ nassumption; ##]
 433     #x; *; #i; #H; napply (Im ? i); napply (subseteq_trans … IH); napply H;
 434 ##| #a; #i; #f; #IH; #x; *; #d; napply IH; ##]
 435 nqed.
 436
 437 nlet rec famF (A: nAx) (F : Ω^A) (x : Ord A) on x : Ω^A ≝
 438   match x with
 439   [ oO ⇒ F
 440   | oS o ⇒ let Fo ≝ famF A F o in Fo ∩ { x | ∀i:𝐈 x.∃j:𝐃 x i.𝐝 x i j ∈ Fo }
 441   | oL a i f ⇒ { x | ∀j:𝐃 a i.x ∈ famF A F (f j) }
 442   ].
 443
 444 interpretation "famF" 'famU U x = (famF ? U x).
 445
 446 ndefinition ord_fished : ∀A:nAx.∀F:Ω^A.Ω^A ≝ λA,F.{ y | ∀x:Ord A. y ∈ F⎽x }.
 447
 448 interpretation "fished new fish" 'fished U = (ord_fished ? U).
 449 interpretation "new fish" 'fish a U = (mem ? (ord_fished ? U) a).
 450
 451 ntheorem new_fish_antirefl:
 452  ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → a ∈ F.
 453 #A; #F; #a; #H; nlapply (H (oO ?)); #aFo; napply aFo;
 454 nqed.
 455
 456 nlemma co_ord_subset:
 457  ∀A:nAx.∀F:Ω^A.∀a,i.∀f:𝐃 a i → Ord A.∀j. F⎽(Λ f) ⊆ F⎽(f j).
 458 #A; #F; #a; #i; #f; #j; #x; #H; napply H;
 459 nqed.
 460
 461 naxiom AC_dual :
 462   ∀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.
 463
 464
 465 ntheorem new_fish_compatible:
 466  ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ⋉ F.
 467 #A; #F; #a; #aF; #i; nnormalize;
 468 napply AC_dual; #f;
 469 nlapply (aF (Λf+1)); #aLf;
 470 nchange in aLf with (a ∈ F⎽(Λ f) ∧ ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ∈ F⎽(Λ f));
 471 ncut (∃j:𝐃 a i.𝐝 a i j ∈ F⎽(f j));##[
 472   ncases aLf; #_; #H; nlapply (H i); *; #j; #Hj; @j; napply Hj;##] #aLf';
 473 napply aLf';
 474 nqed.
 475
 476 ntheorem max_new_fished:
 477   ∀A:nAx.∀G,F:Ω^A.G ⊆ F → (∀a.a ∈ G → ∀i.𝐈𝐦[𝐝 a i] ≬ G) → G ⊆ ⋉F.
 478 #A; #G; #F; #GF; #H; #b; #HbG; #o; ngeneralize in match HbG; ngeneralize in match b;
 479 nchange with (G ⊆ F⎽o);
 480 nelim o;
 481 ##[ napply GF;
 482 ##| #p; #IH; napply (subseteq_intersection_r … IH);
 483     #x; #Hx; #i; ncases (H … Hx i); #c; *; *; #d; #Ed; #cG;
 484     @d; napply IH; napply (setoidification … Ed^-1); napply cG;
 485 ##| #a; #i; #f; #Hf; nchange with (G ⊆ { y | ∀x. y ∈ F⎽(f x) });
 486     #b; #Hb; #d; napply (Hf d); napply Hb;
 487 ##]
 488 nqed.
 489
 490 (*DOCBEGIN
 491
 492 [1]: http://upsilon.cc/~zack/research/publications/notation.pdf
 493
 494 *)