intro i
case right.right
I : Type u₀
C : IContainer I
i✝ : I
x✝ : M C i✝
R : (i : I) → M C i → M C i → Prop := fun i x y => x = construct (destruct y)
i : I
x y : M C i
h₀✝ : R i x y
node : A C i
k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ :
  destruct x =
    { fst := node,
      snd := fun y =>
        corec
          (fun i x =>
            match x with
            | { fst := x, snd := k } => { fst := x, snd := fun y => destruct (k y) })
          (destruct (k₂ y)) }
⊢ ∀ (z : B C i node), R (N C i node z) ((fun x => construct (destruct (k₂ x))) z) (k₂ z)
case right.right
I : Type u₀
C : IContainer I
i✝¹ : I
x✝ : M C i✝¹
R : (i : I) → M C i → M C i → Prop := fun i x y => x = construct (destruct y)
i✝ : I
x y : M C i✝
h₀✝ : R i✝ x y
node : A C i✝
k₂ : (y : B C i✝ node) → M C (N C i✝ node y)
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ :
  destruct x =
    { fst := node,
      snd := fun y =>
        corec
          (fun i x =>
            match x with
            | { fst := x, snd := k } => { fst := x, snd := fun y => destruct (k y) })
          (destruct (k₂ y)) }
i : B C i✝ node
⊢ R (N C i✝ node i) ((fun x => construct (destruct (k₂ x))) i) (k₂ i)