+
+(*D
+
+We similarly define the subset of points "fished" by `F`, the
+equation characterizing `⋉(F)` and prove that fish is
+the biggest solution for such equation.
+
+D*)
+
+notation "⋉F" non associative with precedence 55
+for @{ 'fished $F }.
+
+ndefinition fished : ∀A:Ax.∀F:Ω^A.Ω^A ≝ λA,F.{ a | a ⋉ F }.
+
+interpretation "fished fish" 'fished F = (fished ? F).
+
+ndefinition fish_equation : ∀A:Ax.∀F,X:Ω^A.CProp[0] ≝ λA,F,X.
+ ∀a. a ∈ X ↔ a ∈ F ∧ ∀i:𝐈 a.∃y.y ∈ 𝐂 a i ∧ y ∈ X.
+
+ntheorem fished_fish_equation : ∀A,F. fish_equation A F (⋉F).
+#A; #F; #a; @; (* *; non genera outtype che lega a *) #H; ncases H;
+##[ #b; #bF; #H2; @ bF; #i; ncases (H2 i); #c; *; #cC; #cF; @c; @ cC;
+ napply cF;
+##| #aF; #H1; @ aF; napply H1;
+##]
+nqed.
+
+ntheorem fished_max_fish_equation : ∀A,F,G. fish_equation A F G → G ⊆ ⋉F.
+#A; #F; #G; #H; #a; #aG; napply (fish_rec … aG);
+#b; ncases (H b); #H1; #_; #bG; ncases (H1 bG); #E1; #E2; nassumption;
+nqed.
+
+(*D
+
+Part 2, the new set of axioms
+-----------------------------
+
+Since the name of defined objects (record included) has to be unique
+within the same file, we prefix every field name
+in the new definition of the axiom set with `n`.
+
+D*)
+
+nrecord nAx : Type[1] ≝ {
+ nS:> Type[0];
+ nI: nS → Type[0];
+ nD: ∀a:nS. nI a → Type[0];
+ nd: ∀a:nS. ∀i:nI a. nD a i → nS
+}.
+
+(*D
+
+We again define a notation for the projections, making the
+projected record an implicit argument. Note that, since we already have
+a notation for `𝐈`, we just add another interpretation for it. The
+system, looking at the argument of `𝐈`, will be able to choose
+the correct interpretation.
+
+D*)
+
+notation "𝐃 \sub ( ❨a,\emsp i❩ )" non associative with precedence 70 for @{ 'D $a $i }.
+notation "𝐝 \sub ( ❨a,\emsp i,\emsp j❩ )" non associative with precedence 70 for @{ 'd $a $i $j}.
+
+notation > "𝐃 term 90 a term 90 i" non associative with precedence 70 for @{ 'D $a $i }.
+notation > "𝐝 term 90 a term 90 i term 90 j" non associative with precedence 70 for @{ 'd $a $i $j}.
+
+interpretation "D" 'D a i = (nD ? a i).
+interpretation "d" 'd a i j = (nd ? a i j).
+interpretation "new I" 'I a = (nI ? a).
+
+(*D
+
+The first result the paper presents to motivate the new formulation
+of the axiom set is the possibility to define and old axiom set
+starting from a new one and vice versa. The key definition for
+such construction is the image of d(a,i).
+The paper defines the image as
+
+> Im[d(a,i)] = { d(a,i,j) | j : D(a,i) }
+
+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
+
+Of course this writing is interpreted by the authors as follows
+
+> ∀j:D(a,i). d(a,i,j) ∈ V
+
+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 | … }` of type `S`.
+
+> Im[d(a,i)] = { y | ∃j:D(a,i). y = d(a,i,j) }
+
+This poses no theoretical problems, since `S` is a Type and thus
+equipped with the `Id` equality. If `S` was a setoid, here the equality
+would have been the one of the setoid.
+
+Unless we define two different images, one for stating that 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.
+Since we decided to use `Id` the rewriting always work (the elimination
+principle for `Id` is Leibnitz's equality, that is quantified over
+the context.
+
+The problem that arises if we decide to make `S` a setoid is that
+`V` has to be extensional w.r.t. the equality of `S` (i.e. the characteristic
+functional proposition has to quotient its input with a relation bigger
+than the one of `S`.
+
+> ∀x,y:S. x = y → x ∈ V → y ∈ V
+
+If `V` is a complex construction, the proof may not be trivial.
+
+D*)
+
+include "logic/equality.ma".
+
+ndefinition image ≝ λA:nAx.λa:A.λi. { x | ∃j:𝐃 a i. x = 𝐝 a i j }.
+
+notation > "𝐈𝐦 [𝐝 term 90 a term 90 i]" non associative with precedence 70 for @{ 'Im $a $i }.
+notation < "𝐈𝐦 [𝐝 \sub ( ❨a,\emsp i❩ )]" non associative with precedence 70 for @{ 'Im $a $i }.
+
+interpretation "image" 'Im a i = (image ? a i).
+
+(*D
+
+Thanks to our definition of image, we can define a function mapping a
+new axiom set to an old one and vice versa. Note that in the second
+definition, when we give the `𝐝` component, the projection of the
+Σ-type is inlined (constructed on the fly by `*;`)
+while in the paper it was named `fst`.
+
+D*)
+
+ndefinition Ax_of_nAx : nAx → Ax.
+#A; @ A (nI ?); #a; #i; napply (𝐈𝐦 [𝐝 a i]);
+nqed.
+
+ndefinition nAx_of_Ax : Ax → nAx.
+#A; @ A (I ?);
+##[ #a; #i; napply (Σx:A.x ∈ 𝐂 a i);
+##| #a; #i; *; #x; #_; napply x;
+##]
+nqed.
+
+(*D
+
+We now prove that the two function above form a retraction pair for
+the `C` component of the axiom set. To prove that we face a little
+problem since CIC is not equipped with η-conversion. This means that
+the followin does not hold (where `A` is an axiom set).
+
+> A = (S A, I A, C A)
+
+This can be proved only under a pattern mach over `A`, that means
+that the resulting computation content of the proof is a program
+that computes something only if `A` is a concrete axiom set.
+
+To state the lemma we have to drop notation, and explicitly
+give the axiom set in input to the `C` projection.
+
+D*)
+
+nlemma Ax_nAx_equiv :
+ ∀A:Ax. ∀a,i. C (Ax_of_nAx (nAx_of_Ax A)) a i ⊆ C A a i ∧
+ C A a i ⊆ C (Ax_of_nAx (nAx_of_Ax A)) a i.
+#A; #a; #i; @; #b; #H; (** screenshot "retr-1". *)
+##[ ncases A in a i b H; #S; #I; #C; #a; #i; #b; #H;(** screenshot "retr-2". *)
+ nchange in a with S; nwhd in H; (** screenshot "retr-3". *)
+ ncases H; #x; #E; nrewrite > E; nwhd in x; (** screenshot "retr-4". *)
+ ncases x; #b; #Hb; nnormalize; nassumption;
+##| ncases A in a i b H; #S; #I; #C; #a; #i; #b; #H; @;
+ ##[ @ b; nassumption;
+ ##| nnormalize; @; ##]
+##]
+nqed.
+
+(*D
+D[retr-1]
+Look for example the type of `a`. The command `nchange in a with A`
+would fail because of the missing η-conversion rule. We have thus
+to pattern match over `A` and introduce its pieces.
+
+D[retr-2]
+Now the system accepts that the type of `a` is the fist component
+of the axiom set, now called `S`. Unfolding definitions in `H` we discover
+there is still some work to do.
+
+D[retr-3]
+To use the equation defining `b` we have to eliminate `H`. Unfolding
+definitions in `x` tell us there is still something to do. The `nrewrite`
+tactic is a shortcut for the elimination principle of the equality.
+It accepts an additional argument `<` or `>` to rewrite left-to-right
+or right-to-left.
+
+D[retr-4]
+We defined `𝐝` to be the first projection of `x`, thus we have to
+eliminate `x` to actually compute `𝐝`.
+
+The remaining part of the proof it not interesting and poses no
+new problems.
+
+D*)
+
+(*D
+
+We then define the inductive type of ordinals, parametrized over an axiom
+set. We also attach some notations to the constructors.
+
+D*)
+
+ninductive Ord (A : nAx) : Type[0] ≝
+ | oO : Ord A
+ | oS : Ord A → Ord A
+ | oL : ∀a:A.∀i.∀f:𝐃 a i → Ord A. Ord A.
+
+notation "0" non associative with precedence 90 for @{ 'oO }.
+notation "x+1" non associative with precedence 50 for @{'oS $x }.
+notation "Λ term 90 f" non associative with precedence 50 for @{ 'oL $f }.
+
+interpretation "ordinals Zero" 'oO = (oO ?).
+interpretation "ordinals Succ" 'oS x = (oS ? x).
+interpretation "ordinals Lambda" 'oL f = (oL ? ? ? f).
+
+(*D
+
+The definition of `U⎽x` is by recursion over the ordinal `x`.
+We thus define a recursive function using the `nlet rec` command.
+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.
+
+D*)
+
+nlet rec famU (A : nAx) (U : Ω^A) (x : Ord A) on x : Ω^A ≝
+ match x with
+ [ oO ⇒ U
+ | 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 }.
+notation > "U ⎽ term 90 x" non associative with precedence 50 for @{ 'famU $U $x }.
+
+interpretation "famU" 'famU U x = (famU ? U x).
+
+(*D
+
+We attach as the input notation for U_x the similar `U⎽x` where underscore,
+that is a character valid for identifier names, has been replaced by `⎽` that is
+not. The symbol `⎽` can act as a separator, and can be typed as an alternative
+for `_` (i.e. pressing ALT-L after `_`).
+
+The notion ◃(U) has to be defined as the subset of elements `y`
+belonging to `U⎽x` for some `x`. Moreover, we have to define the notion
+of cover between sets again, since the one defined at the beginning
+of the tutorial works only for the old axiom set.
+
+D*)
+
+ndefinition ord_coverage : ∀A:nAx.∀U:Ω^A.Ω^A ≝
+ λA,U.{ y | ∃x:Ord A. y ∈ famU ? U x }.
+
+ndefinition ord_cover_set ≝ λc:∀A:nAx.Ω^A → Ω^A.λA,C,U.
+ ∀y.y ∈ C → y ∈ c A U.
+
+interpretation "coverage new cover" 'coverage U = (ord_coverage ? U).
+interpretation "new covers set" 'covers a U = (ord_cover_set ord_coverage ? a U).
+interpretation "new covers" 'covers a U = (mem ? (ord_coverage ? U) a).
+
+(*D
+
+Before proving that this cover relation validates the reflexivity and infinity
+rules, we prove this little technical lemma that is used in the proof for the
+infinity rule.
+
+D*)
+
+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.
+
+(*D
+
+The proof of infinity uses the following form of the Axiom of Choice,
+that cannot be proved inside Matita, since the existential quantifier
+lives in the sort of predicative propositions while the sigma in the conclusion
+lives in the sort of data types, and thus the former cannot be eliminated
+to provide the witness for the second.
+
+D*)
+
+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)).
+
+(*D
+
+Note that, if we will decide later to identify ∃ and Σ, `AC` is
+trivially provable
+
+D*)
+
+nlemma AC_exists_is_sigma : ∀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)).
+#A; #a; #i; #U; #H; @;
+##[ #j; ncases (H j); #x; #_; napply x;
+##| #j; ncases (H j); #x; #Hx; napply Hx; ##]
+nqed.
+
+(*D
+
+In case we made `S` a setoid, the following property has to be proved
+
+> nlemma U_x_is_ext: ∀A:nAx.∀a,b:A.∀x.∀U. a = b → b ∈ U⎽x → a ∈ U⎽x.
+
+Anyway this proof is a non trivial induction over x, that requires `𝐈` and `𝐃` to be
+declared as morphisms.
+
+D*)
+
+
+(*D
+
+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. Note that `0` is between `(` and `)` to
+make it clear that it is a term (an ordinal) and not the number
+of the constructor we want to apply (that is the first and only one
+of the existential inductive type).
+
+D*)
+ntheorem new_coverage_reflexive: ∀A:nAx.∀U:Ω^A.∀a. a ∈ U → a ◃ U.
+#A; #U; #a; #H; @ (0); napply H;
+nqed.
+
+(*D
+
+We now proceed with the proof of the infinity rule.
+
+D*)
+
+alias symbol "covers" (instance 3) = "new covers set".
+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". *)
+*; #i; #H; nnormalize in H; (** screenshot "n-cov-inf-2". *)
+ncut (∀y:𝐃 a i.∃x:Ord A.𝐝 a i y ∈ U⎽x); ##[ (** screenshot "n-cov-inf-3". *)
+ #z; napply H; @ z; @; ##] #H'; (** screenshot "n-cov-inf-4". *)
+ncases (AC … H'); #f; #Hf; (** screenshot "n-cov-inf-5". *)
+ncut (∀j.𝐝 a i j ∈ U⎽(Λ f));
+ ##[ #j; napply (ord_subset … f … (Hf j));##] #Hf';(** screenshot "n-cov-inf-6". *)
+@ (Λ f+1); (** screenshot "n-cov-inf-7". *)
+@2; (** screenshot "n-cov-inf-8". *)
+@i; #x; *; #d; #Hd; (** screenshot "n-cov-inf-9". *)
+nrewrite > Hd; napply Hf';
+nqed.
+
+(*D
+D[n-cov-inf-1]
+We eliminate the existential, obtaining an `i` and a proof that the
+image of `𝐝 a i` is covered by U. The `nnormalize` tactic computes the normal
+form of `H`, thus expands the definition of cover between sets.
+
+D[n-cov-inf-2]
+When the paper proof considers `H`, it implicitly substitutes assumed
+equation defining `y` in its conclusion.
+In Matita this step is not completely trivial.
+We thus assert (`ncut`) the nicer form of `H` and prove it.
+
+D[n-cov-inf-3]
+After introducing `z`, `H` can be applied (choosing `𝐝 a i z` as `y`).
+What is the left to prove is that `∃j: 𝐃 a j. 𝐝 a i z = 𝐝 a i j`, that
+becomes trivial if `j` is chosen to be `z`.
+
+D[n-cov-inf-4]
+Under `H'` the axiom of choice `AC` can be eliminated, obtaining the `f` and
+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
+lemma we proved above) `Hf'` i.e. 𝐝 a i j ∈ U⎽(Λf).
+
+D[n-cov-inf-6]
+To prove that `a◃U` we have to exhibit the ordinal x such that `a ∈ U⎽x`.
+
+D[n-cov-inf-7]
+The definition of `U⎽(…+1)` expands to the union of two sets, and proving
+that `a ∈ X ∪ Y` is, by definition, equivalent to prove that `a` is in `X` or `Y`.
+Applying the second constructor `@2;` of the disjunction,
+we are left to prove that `a` belongs to the right hand side of the union.
+
+D[n-cov-inf-8]
+We thus provide `i` as the witness of the existential, introduce the
+element being in the image and we are
+left to prove that it belongs to `U⎽(Λf)`. In the meanwhile, since belonging
+to the image means that there exists an object in the domain …, we eliminate the
+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
+every `x`, thus we are allowed to use `Hd` and close the proof.
+
+D*)
+
+(*D
+
+The next proof is that ◃(U) is minimal. The hardest part of the proof
+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:
+
+> ∀x. x ∈ { y | ∃o:Ord A.y ∈ U⎽o } → x ∈ V
+
+D*)
+
+nlemma new_coverage_min :
+ ∀A:nAx.∀U:Ω^A.∀V.U ⊆ V → (∀a:A.∀i.𝐈𝐦[𝐝 a i] ⊆ V → a ∈ V) → ◃U ⊆ V.
+#A; #U; #V; #HUV; #Im;#b; (** screenshot "n-cov-min-2". *)
+*; #o; (** screenshot "n-cov-min-3". *)
+ngeneralize in match b; nchange with (U⎽o ⊆ V); (** screenshot "n-cov-min-4". *)
+nelim o; (** screenshot "n-cov-min-5". *)
+##[ napply HUV;
+##| #p; #IH; napply subseteq_union_l; ##[ nassumption; ##]
+ #x; *; #i; #H; napply (Im ? i); napply (subseteq_trans … IH); napply H;
+##| #a; #i; #f; #IH; #x; *; #d; napply IH; ##]
+nqed.
+
+(*D
+D[n-cov-min-2]
+After all the introductions, event the element hidden in the ⊆ definition,
+we have to eliminate the existential quantifier, obtaining the ordinal `o`
+
+D[n-cov-min-3]
+What is left is almost right, but the element `b` is already in the
+context. We thus generalize every occurrence of `b` in
+the current goal, obtaining `∀c.c ∈ U⎽o → c ∈ V` that is `U⎽o ⊆ V`.
+
+D[n-cov-min-4]
+We then proceed by induction on `o` obtaining the following goals
+
+D[n-cov-min-5]
+All of them can be proved using simple set theoretic arguments,
+the induction hypothesis and the assumption `Im`.
+
+D*)
+
+
+(*D
+
+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 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) }
+ ].
+
+interpretation "famF" 'famU U x = (famF ? U x).
+
+ndefinition ord_fished : ∀A:nAx.∀F:Ω^A.Ω^A ≝ λA,F.{ y | ∀x:Ord A. y ∈ F⎽x }.
+
+interpretation "fished new fish" 'fished U = (ord_fished ? U).
+interpretation "new fish" 'fish a U = (mem ? (ord_fished ? U) a).
+
+(*D
+
+The proof of compatibility uses this little result, that we
+proved outside the main proof.
+
+D*)
+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.
+
+(*D
+
+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.
+
+(*D
+
+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 choose to be `0`, we obtain the thesis.
+
+D*)
+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
+
+We now prove the compatibility property for the new fish relation.
+
+D*)
+ntheorem new_fish_compatible:
+ ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ⋉ F.
+#A; #F; #a; #aF; #i; nnormalize; (** screenshot "n-f-compat-1". *)
+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". *)
+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 observe it is exactly the conclusion 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 be computed.
+Anyway, using the `nnormalize`
+tactic would reduce too much (both the `+1` and the `Λf` steps would be performed);
+we thus explicitly give a convertible type for that hypothesis, corresponding
+the computation of the `+1` step, plus the unfolding the definition of
+the intersection.
+
+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*)
+
+(*D
+
+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`.
+
+D*)
+ntheorem max_new_fished:
+ ∀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);
+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; (** screenshot "n-f-max-1". *)
+ nrewrite < Ed; napply cG;
+##| #a; #i; #f; #Hf; nchange with (G ⊆ { y | ∀x. y ∈ F⎽(f x) });
+ #b; #Hb; #d; napply (Hf d); napply Hb;