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 ↑node), R (Next C (↑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 : C.A
h₄ : i = Idx C node
k₁ k₂ : (y : B C ↑{ val := node, property := h₄ }) → M C (Next C (↑{ val := node, property := h₄ }) y)
h₁✝ : destruct { val := x, property := wfx } = { fst := { val := node, property := h₄ }, snd := k₁ }
h₂✝ : destruct { val := y, property := wfy } = { fst := { val := node, property := h₄ }, snd := k₂ }
h₃ : ∀ (z : B C ↑{ val := node, property := h₄ }), R (Next C (↑{ val := node, property := h₄ }) z) (k₁ z) (k₂ z)
h₁ :
  Container.M.destruct x =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }
h₂ :
  Container.M.destruct y =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₂ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₂ } x) }
wfx' :
  ∀ (x_1 : B C (Container.M.destruct ↑{ val := x, property := wfx }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := x, property := wfx }).fst x_1)
      (PSigma.snd (Container.M.destruct ↑{ val := x, property := wfx }) x_1)
wfy' :
  ∀ (x : B C (Container.M.destruct ↑{ val := y, property := wfy }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := y, property := wfy }).fst x)
      (PSigma.snd (Container.M.destruct ↑{ val := y, property := wfy }) x)
a : B C node
⊢ ∃ h,
    R (Next C node a) { val := ↑(k₁ a), property := (_ : WellFormed (Next C node a) ((fun a => ↑(k₁ a)) a)) }
      { val := ↑(k₂ a), property := (_ : WellFormed (Next C node a) ((fun x => ↑(k₂ x)) a)) }
Tactic:
exists (by
    rw [h₂] at wfy'
    apply wfy'
  )
Proof state after:
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 ↑node), R (Next C (↑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 : C.A
h₄ : i = Idx C node
k₁ k₂ : (y : B C ↑{ val := node, property := h₄ }) → M C (Next C (↑{ val := node, property := h₄ }) y)
h₁✝ : destruct { val := x, property := wfx } = { fst := { val := node, property := h₄ }, snd := k₁ }
h₂✝ : destruct { val := y, property := wfy } = { fst := { val := node, property := h₄ }, snd := k₂ }
h₃ : ∀ (z : B C ↑{ val := node, property := h₄ }), R (Next C (↑{ val := node, property := h₄ }) z) (k₁ z) (k₂ z)
h₁ :
  Container.M.destruct x =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }
h₂ :
  Container.M.destruct y =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₂ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₂ } x) }
wfx' :
  ∀ (x_1 : B C (Container.M.destruct ↑{ val := x, property := wfx }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := x, property := wfx }).fst x_1)
      (PSigma.snd (Container.M.destruct ↑{ val := x, property := wfx }) x_1)
wfy' :
  ∀ (x : B C (Container.M.destruct ↑{ val := y, property := wfy }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := y, property := wfy }).fst x)
      (PSigma.snd (Container.M.destruct ↑{ val := y, property := wfy }) x)
a : B C node
⊢ R (Next C node a) { val := ↑(k₁ a), property := (_ : WellFormed (Next C node a) ((fun a => ↑(k₁ a)) a)) }
    { val := ↑(k₂ a), property := (_ : WellFormed (Next C node a) ((fun x => ↑(k₂ x)) a)) }