Theorem: IContainer.M.bisim
Proof state before:
case h₀.right.left
I : Type u₀
C : IContainer I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁✝ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
node : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct x).fst.fst
hiy : i = (Container.M.destruct y).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
⊢ Container.M.destruct y = { fst := { fst := i, snd := node }, snd := fun x => ↑(k₂ x) }

case h₀.right.right
I : Type u₀
C : IContainer I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁✝ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
node : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct x).fst.fst
hiy : i = (Container.M.destruct y).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
⊢ ∀ (i_1 : Container.B (toContainer C) { fst := i, snd := node }),
    ∃ i_2 wfx wfy,
      R i_2 { val := (fun x => ↑(k₁ x)) i_1, property := wfx } { val := (fun x => ↑(k₂ x)) i_1, property := wfy }
Tactic:
. cases hiy
  have hny: ny = node := by
    apply congrArg Sigma.fst h₂
  cases hny
  have h₂ := Sigma.snd_equals _ _ _ h₂
  rw [← h₂]
  rfl
Proof state after:
case h₀.right.right
I : Type u₀
C : IContainer I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁✝ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
node : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct x).fst.fst
hiy : i = (Container.M.destruct y).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
⊢ ∀ (i_1 : Container.B (toContainer C) { fst := i, snd := node }),
    ∃ i_2 wfx wfy,
      R i_2 { val := (fun x => ↑(k₁ x)) i_1, property := wfx } { val := (fun x => ↑(k₂ x)) i_1, property := wfy }