+
+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 }
+ | 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).
+
+ntheorem new_fish_antirefl:
+ ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → a ∈ F.
+#A; #F; #a; #H; nlapply (H (oO ?)); #aFo; napply aFo;
+nqed.
+
+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.
+
+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.
+
+
+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;
+napply AC_dual; #f;
+nlapply (aF (Λf+1)); #aLf;
+nchange in aLf with (a ∈ F⎽(Λ f) ∧ ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ∈ F⎽(Λ f));
+ncut (∃j:𝐃 a i.𝐝 a i j ∈ F⎽(f j));##[
+ ncases aLf; #_; #H; nlapply (H i); *; #j; #Hj; @j; napply Hj;##] #aLf';
+napply aLf';
+nqed.
+
+(* 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_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.