# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1688195034 -32400
# Node ID 800218d431dc0b0ee55986b31fcbf3f7fa5be2b9
# Parent  a0e8df81a466580f2604052f0817f0f5bc84537f
...

diff -r a0e8df81a466 -r 800218d431dc src/cardinal.agda
--- a/src/cardinal.agda	Sat Jul 01 16:03:42 2023 +0900
+++ b/src/cardinal.agda	Sat Jul 01 16:03:54 2023 +0900
@@ -429,6 +429,14 @@
            be77 : odef (* (& a-UC)) (fba x (proj1 (subst (λ k → odef k x) *iso be76)))
            be77 = subst (λ k → odef k (fba x (proj1 (subst (λ k → odef k x) *iso be76)) )) (sym *iso) 
                ⟪ a∋fba x (proj1 (subst (λ k → odef k x) *iso be76)) , ? ⟫
+           be78 : fba x (proj1 (subst (λ k → odef k x) *iso be76)) p
+              (sym *iso) ⟪ proj1 (subst₂ (λ A → OD.def (od A)) *iso refl (subst (λ k → OD.def (od k) (fba x
+                    (proj1 (subst (λ k₁ → OD.def (od k₁) x) *iso (subst (λ k₁ → OD.def (od k₁) x) (sym *iso)
+                       ⟪ bx , subst (λ k₁ → OD.def (od k₁) x → ⊥) (sym *iso) x₁ ⟫))))) (sym *iso)
+                ⟪ a∋fba x (proj1 (subst (λ k → OD.def (od k) x) *iso (subst (λ k → OD.def (od k) x) (sym *iso)
+                   ⟪ bx , subst (λ k → OD.def (od k) x → ⊥) (sym *iso) x₁ ⟫))) , (λ cn →
+                   cardinal.be25 O fab b∋fab fab-inject fba a∋fba fba-inject x (subst (λ k → OD.def (od k) x) (sym *iso)
+                    ⟪ bx , subst (λ k → OD.def (od k) x → ⊥) (sym *iso) x₁ ⟫) cn | cn) ⟫)) , c2 ⟫))
 
 
       be73 :  (x : Ordinal) (ax : odef (* a) x) → (cc0 : CC0 x ) →  h⁻¹ (be70 x ax cc0) (cc11 ax cc0) ≡ x