Theorem: Container.M.construct_destruct (CoInd/Utils.lean)

State before:
C : Container
x : M C
⊢ construct (destruct x) = x
Tactic:
let R (x y: M C) := x = construct (destruct y)
State after:
C : Container
x : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
⊢ construct (destruct x) = x

State before:
C : Container
x : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
⊢ construct (destruct x) = x
Tactic:
apply bisim R
State after:
case h₀
C : Container
x : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
⊢ ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)

case a
C : Container
x : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
⊢ R (construct (destruct x)) x

State before:
case h₀
C : Container
x : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
⊢ ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)

case a
C : Container
x : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
⊢ R (construct (destruct x)) x
Tactic:
. intro x y h₀
  have h₀ := congrArg destruct h₀
  cases h₁:destruct y
  case mk node k₂ =>
    rw [h₁] at h₀
    simp only [construct, destruct_corec, Map] at h₀
    simp only [construct.automaton, Map] at h₀
    exists node
    exists construct ∘ destruct ∘ k₂
    exists k₂
    constructor
    . exact h₀
    . constructor
      . rfl
      . intro i
        rfl
State after:
case a
C : Container
x : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
⊢ R (construct (destruct x)) x

State before:
case a
C : Container
x : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
⊢ R (construct (destruct x)) x
Tactic:
. rfl
State after:
no goals

State before:
case h₀
C : Container
x : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
⊢ ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
Tactic:
intro x y h₀
State after:
case h₀
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀ : R x y
⊢ ∃ node k₁ k₂,
    destruct x = { fst := node, snd := k₁ } ∧
      destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)

State before:
case h₀
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀ : R x y
⊢ ∃ node k₁ k₂,
    destruct x = { fst := node, snd := k₁ } ∧
      destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
Tactic:
have h₀ := congrArg destruct h₀
State after:
case h₀
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
h₀ : destruct x = destruct (construct (destruct y))
⊢ ∃ node k₁ k₂,
    destruct x = { fst := node, snd := k₁ } ∧
      destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)

State before:
case h₀
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
h₀ : destruct x = destruct (construct (destruct y))
⊢ ∃ node k₁ k₂,
    destruct x = { fst := node, snd := k₁ } ∧
      destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
Tactic:
cases h₁:destruct y
State after:
case h₀.mk
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
h₀ : destruct x = destruct (construct (destruct y))
fst✝ : C.A
snd✝ : B C fst✝ → M C
h₁ : destruct y = { fst := fst✝, snd := snd✝ }
⊢ ∃ node k₁ k₂,
    destruct x = { fst := node, snd := k₁ } ∧
      { fst := fst✝, snd := snd✝ } = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)

State before:
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
h₀ : destruct x = destruct (construct (destruct y))
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
⊢ ∃ node_1 k₁ k₂_1,
    destruct x = { fst := node_1, snd := k₁ } ∧
      { fst := node, snd := k₂ } = { fst := node_1, snd := k₂_1 } ∧ ∀ (i : B C node_1), R (k₁ i) (k₂_1 i)
Tactic:
case mk node k₂ =>
  rw [h₁] at h₀
  simp only [construct, destruct_corec, Map] at h₀
  simp only [construct.automaton, Map] at h₀
  exists node
  exists construct ∘ destruct ∘ k₂
  exists k₂
  constructor
  . exact h₀
  . constructor
    . rfl
    . intro i
      rfl
State after:
no goals

State before:
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
h₀ : destruct x = destruct (construct (destruct y))
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
⊢ ∃ node_1 k₁ k₂_1,
    destruct x = { fst := node_1, snd := k₁ } ∧
      { fst := node, snd := k₂ } = { fst := node_1, snd := k₂_1 } ∧ ∀ (i : B C node_1), R (k₁ i) (k₂_1 i)
Tactic:
rw [h₁] at h₀
State after:
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₀ : destruct x = destruct (construct { fst := node, snd := k₂ })
h₁ : destruct y = { fst := node, snd := k₂ }
⊢ ∃ node_1 k₁ k₂_1,
    destruct x = { fst := node_1, snd := k₁ } ∧
      { fst := node, snd := k₂ } = { fst := node_1, snd := k₂_1 } ∧ ∀ (i : B C node_1), R (k₁ i) (k₂_1 i)

State before:
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₀ : destruct x = destruct (construct { fst := node, snd := k₂ })
h₁ : destruct y = { fst := node, snd := k₂ }
⊢ ∃ node_1 k₁ k₂_1,
    destruct x = { fst := node_1, snd := k₁ } ∧
      { fst := node, snd := k₂ } = { fst := node_1, snd := k₂_1 } ∧ ∀ (i : B C node_1), R (k₁ i) (k₂_1 i)
Tactic:
simp only [construct, destruct_corec, Map] at h₀
State after:
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ :
  destruct x =
    { fst := (construct.automaton { fst := node, snd := k₂ }).fst,
      snd := corec construct.automaton ∘ (construct.automaton { fst := node, snd := k₂ }).snd }
⊢ ∃ node_1 k₁ k₂_1,
    destruct x = { fst := node_1, snd := k₁ } ∧
      { fst := node, snd := k₂ } = { fst := node_1, snd := k₂_1 } ∧ ∀ (i : B C node_1), R (k₁ i) (k₂_1 i)

State before:
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ :
  destruct x =
    { fst := (construct.automaton { fst := node, snd := k₂ }).fst,
      snd := corec construct.automaton ∘ (construct.automaton { fst := node, snd := k₂ }).snd }
⊢ ∃ node_1 k₁ k₂_1,
    destruct x = { fst := node_1, snd := k₁ } ∧
      { fst := node, snd := k₂ } = { fst := node_1, snd := k₂_1 } ∧ ∀ (i : B C node_1), R (k₁ i) (k₂_1 i)
Tactic:
simp only [construct.automaton, Map] at h₀
State after:
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ ∃ node_1 k₁ k₂_1,
    destruct x = { fst := node_1, snd := k₁ } ∧
      { fst := node, snd := k₂ } = { fst := node_1, snd := k₂_1 } ∧ ∀ (i : B C node_1), R (k₁ i) (k₂_1 i)

State before:
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ ∃ node_1 k₁ k₂_1,
    destruct x = { fst := node_1, snd := k₁ } ∧
      { fst := node, snd := k₂ } = { fst := node_1, snd := k₂_1 } ∧ ∀ (i : B C node_1), R (k₁ i) (k₂_1 i)
Tactic:
exists node
State after:
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ ∃ k₁ k₂_1,
    destruct x = { fst := node, snd := k₁ } ∧
      { fst := node, snd := k₂ } = { fst := node, snd := k₂_1 } ∧ ∀ (i : B C node), R (k₁ i) (k₂_1 i)

State before:
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ ∃ k₁ k₂_1,
    destruct x = { fst := node, snd := k₁ } ∧
      { fst := node, snd := k₂ } = { fst := node, snd := k₂_1 } ∧ ∀ (i : B C node), R (k₁ i) (k₂_1 i)
Tactic:
exists construct ∘ destruct ∘ k₂
State after:
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ ∃ k₂_1,
    destruct x = { fst := node, snd := construct ∘ destruct ∘ k₂ } ∧
      { fst := node, snd := k₂ } = { fst := node, snd := k₂_1 } ∧
        ∀ (i : B C node), R ((construct ∘ destruct ∘ k₂) i) (k₂_1 i)

State before:
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ ∃ k₂_1,
    destruct x = { fst := node, snd := construct ∘ destruct ∘ k₂ } ∧
      { fst := node, snd := k₂ } = { fst := node, snd := k₂_1 } ∧
        ∀ (i : B C node), R ((construct ∘ destruct ∘ k₂) i) (k₂_1 i)
Tactic:
exists k₂
State after:
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ destruct x = { fst := node, snd := construct ∘ destruct ∘ k₂ } ∧
    { fst := node, snd := k₂ } = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R ((construct ∘ destruct ∘ k₂) i) (k₂ i)

State before:
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ destruct x = { fst := node, snd := construct ∘ destruct ∘ k₂ } ∧
    { fst := node, snd := k₂ } = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R ((construct ∘ destruct ∘ k₂) i) (k₂ i)
Tactic:
constructor
State after:
case left
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ destruct x = { fst := node, snd := construct ∘ destruct ∘ k₂ }

case right
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ { fst := node, snd := k₂ } = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R ((construct ∘ destruct ∘ k₂) i) (k₂ i)

State before:
case left
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ destruct x = { fst := node, snd := construct ∘ destruct ∘ k₂ }

case right
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ { fst := node, snd := k₂ } = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R ((construct ∘ destruct ∘ k₂) i) (k₂ i)
Tactic:
. exact h₀
State after:
case right
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ { fst := node, snd := k₂ } = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R ((construct ∘ destruct ∘ k₂) i) (k₂ i)

State before:
case right
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ { fst := node, snd := k₂ } = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R ((construct ∘ destruct ∘ k₂) i) (k₂ i)
Tactic:
. constructor
  . rfl
  . intro i
    rfl
State after:
no goals

State before:
case left
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ destruct x = { fst := node, snd := construct ∘ destruct ∘ k₂ }
Tactic:
exact h₀
State after:
no goals

State before:
case right
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ { fst := node, snd := k₂ } = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R ((construct ∘ destruct ∘ k₂) i) (k₂ i)
Tactic:
constructor
State after:
case right.left
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ { fst := node, snd := k₂ } = { fst := node, snd := k₂ }

case right.right
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ ∀ (i : B C node), R ((construct ∘ destruct ∘ k₂) i) (k₂ i)

State before:
case right.left
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ { fst := node, snd := k₂ } = { fst := node, snd := k₂ }

case right.right
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ ∀ (i : B C node), R ((construct ∘ destruct ∘ k₂) i) (k₂ i)
Tactic:
. rfl
State after:
case right.right
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ ∀ (i : B C node), R ((construct ∘ destruct ∘ k₂) i) (k₂ i)

State before:
case right.right
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ ∀ (i : B C node), R ((construct ∘ destruct ∘ k₂) i) (k₂ i)
Tactic:
. intro i
  rfl
State after:
no goals

State before:
case right.left
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ { fst := node, snd := k₂ } = { fst := node, snd := k₂ }
Tactic:
rfl
State after:
no goals

State before:
case right.right
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ ∀ (i : B C node), R ((construct ∘ destruct ∘ k₂) i) (k₂ i)
Tactic:
intro i
State after:
case right.right
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
i : B C node
⊢ R ((construct ∘ destruct ∘ k₂) i) (k₂ i)

State before:
case right.right
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
i : B C node
⊢ R ((construct ∘ destruct ∘ k₂) i) (k₂ i)
Tactic:
rfl
State after:
no goals

State before:
case a
C : Container
x : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
⊢ R (construct (destruct x)) x
Tactic:
rfl
State after:
no goals