Theorem: IContainer.M.bisim
Proof state before:
case h₀.right.left.refl
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)
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
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)
wfx : WellFormed (Container.M.destruct y).fst.fst x
wfy : WellFormed (Container.M.destruct y).fst.fst y
r : R (Container.M.destruct y).fst.fst { val := x, property := wfx } { val := y, property := wfy }
node : A C (Container.M.destruct y).fst.fst
k₁ k₂ : (y_1 : B C (Container.M.destruct y).fst.fst node) → M C (N C (Container.M.destruct y).fst.fst node y_1)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct y).fst.fst node), R (N C (Container.M.destruct y).fst.fst node z) (k₁ z) (k₂ z)
hix : (Container.M.destruct y).fst.fst = (Container.M.destruct x).fst.fst
⊢ Container.M.destruct y = { fst := { fst := (Container.M.destruct y).fst.fst, snd := node }, snd := fun x => ↑(k₂ x) }
Tactic:
have hny: ny = node := by
  apply congrArg Sigma.fst h₂
Proof state after:
case h₀.right.left.refl
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)
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
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)
wfx : WellFormed (Container.M.destruct y).fst.fst x
wfy : WellFormed (Container.M.destruct y).fst.fst y
r : R (Container.M.destruct y).fst.fst { val := x, property := wfx } { val := y, property := wfy }
node : A C (Container.M.destruct y).fst.fst
k₁ k₂ : (y_1 : B C (Container.M.destruct y).fst.fst node) → M C (N C (Container.M.destruct y).fst.fst node y_1)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct y).fst.fst node), R (N C (Container.M.destruct y).fst.fst node z) (k₁ z) (k₂ z)
hix : (Container.M.destruct y).fst.fst = (Container.M.destruct x).fst.fst
hny : ny = node
⊢ Container.M.destruct y = { fst := { fst := (Container.M.destruct y).fst.fst, snd := node }, snd := fun x => ↑(k₂ x) }