Theorem: IContainer.M.bisim
Proof state before:
case h₀
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 wfx wfy, R i { val := x, property := wfx } { val := y, property := wfy }) →
      ∃ node k₁ k₂,
        Container.M.destruct x = { fst := node, snd := k₁ } ∧
          Container.M.destruct y = { fst := node, snd := k₂ } ∧
            ∀ (i : Container.B (toContainer C) node),
              ∃ i_1 wfx wfy, R i_1 { val := k₁ i, property := wfx } { val := k₂ i, property := wfy }

case a
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 }
⊢ ∃ i wfx wfy, R i { val := x, property := wfx } { val := y, property := wfy }
Tactic:
. intro x y ⟨i, wfx, wfy, r⟩
  have ⟨node, k₁, k₂, h₁, h₂, h₃⟩ := h₀ i ⟨x, wfx⟩ ⟨y, wfy⟩ r
  let ix := (Container.M.destruct x).1.1
  let nx := (Container.M.destruct x).1.2
  let kx := (Container.M.destruct x).2
  let iy := (Container.M.destruct y).1.1
  let ny := (Container.M.destruct y).1.2
  let ky := (Container.M.destruct y).2
  have hix := index_destruct ⟨x, wfx⟩
  have hiy := index_destruct ⟨y, wfy⟩
  have wfx' : ∀ a:B C ix nx, WellFormed (C.N ix nx a) (kx a) := wf_destruct ⟨x, wfx⟩
  have wfy' : ∀ a:B C iy ny, WellFormed (C.N iy ny a) (ky a) := wf_destruct ⟨y, wfy⟩
  simp only at hix hiy wfx wfy
  exists ⟨_, node⟩
  exists λ x => (k₁ x).1
  exists λ x => (k₂ x).1
  constructor
  . cases hix
    have hnx: nx = node := by
      apply congrArg Sigma.fst h₁
    cases hnx
    have h₁ := Sigma.snd_equals _ _ _ h₁
    rw [← h₁]
    rfl
  . constructor
    . cases hiy
      have hny: ny = node := by
        apply congrArg Sigma.fst h₂
      cases hny
      have h₂ := Sigma.snd_equals _ _ _ h₂
      rw [← h₂]
      rfl
    . intro a
      exists C.N i node a
      simp only [toContainer] at a
      exists (by
          cases hix
          have : nx = node := by
            apply congrArg Sigma.fst h₁
          cases this
          have h₁ := Sigma.snd_equals _ _ _ h₁
          have wfx' := wfx' a
          cases h₁
          exact wfx'
        )
      exists (by
          cases hiy
          have : ny = node := by
            apply congrArg Sigma.fst h₂
          cases this
          have h₂ := Sigma.snd_equals _ _ _ h₂
          have wfy' := wfy' a
          cases h₂
          exact wfy'
        )
      exact h₃ a
Proof state after:
case a
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 }
⊢ ∃ i wfx wfy, R i { val := x, property := wfx } { val := y, property := wfy }