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

State before:
I : Type u₀
C : IContainer I
i : I
x : M C i
⊢ construct (destruct x) = x
Tactic:
let R i (x y: M C i) := x = construct (destruct y)
State after:
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)
⊢ construct (destruct x) = x

State before:
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)
⊢ construct (destruct x) = x
Tactic:
apply bisim R
State after:
case h₀
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),
    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)

case a
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)
⊢ R i (construct (destruct x)) x

State before:
case h₀
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),
    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)

case a
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)
⊢ R i (construct (destruct x)) x
Tactic:
. intro i 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 λ (x:B C i node) => construct <| destruct <| k₂ x
    exists k₂
    constructor
    . exact h₀
    . constructor
      . rfl
      . intro i
        rfl
State after:
case a
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)
⊢ R i (construct (destruct x)) x

State before:
case a
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)
⊢ R i (construct (destruct x)) x
Tactic:
. rfl
State after:
no goals

State before:
case h₀
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),
    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)
Tactic:
intro i x y h₀
State after:
case h₀
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 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)

State before:
case h₀
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 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)
Tactic:
have h₀ := congrArg destruct h₀
State after:
case h₀
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
h₀ : destruct x = destruct (construct (destruct 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)

State before:
case h₀
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
h₀ : destruct x = destruct (construct (destruct 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)
Tactic:
cases h₁:destruct y
State after:
case h₀.mk
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
h₀ : destruct x = destruct (construct (destruct y))
fst✝ : A C i
snd✝ : (y : B C i fst✝) → M C (N C i fst✝ y)
h₁ : destruct y = { fst := fst✝, snd := snd✝ }
⊢ ∃ node k₁ k₂,
    destruct x = { fst := node, snd := k₁ } ∧
      { fst := fst✝, snd := snd✝ } = { fst := node, snd := k₂ } ∧ ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)

State before:
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
h₀ : destruct x = destruct (construct (destruct 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₂ }
⊢ ∃ node_1 k₁ k₂_1,
    destruct x = { fst := node_1, snd := k₁ } ∧
      { fst := node, snd := k₂ } = { fst := node_1, snd := k₂_1 } ∧
        ∀ (z : B C i node_1), R (N C i node_1 z) (k₁ z) (k₂_1 z)
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 λ (x:B C i node) => construct <| destruct <| k₂ x
  exists k₂
  constructor
  . exact h₀
  . constructor
    . rfl
    . intro i
      rfl
State after:
no goals

State before:
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
h₀ : destruct x = destruct (construct (destruct 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₂ }
⊢ ∃ node_1 k₁ k₂_1,
    destruct x = { fst := node_1, snd := k₁ } ∧
      { fst := node, snd := k₂ } = { fst := node_1, snd := k₂_1 } ∧
        ∀ (z : B C i node_1), R (N C i node_1 z) (k₁ z) (k₂_1 z)
Tactic:
rw [h₁] at h₀
State after:
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 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 } ∧
        ∀ (z : B C i node_1), R (N C i node_1 z) (k₁ z) (k₂_1 z)

State before:
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 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 } ∧
        ∀ (z : B C i node_1), R (N C i node_1 z) (k₁ z) (k₂_1 z)
Tactic:
simp only [construct, destruct_corec, Map] at h₀
State after:
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 =
    match construct.automaton i { fst := node, snd := k₂ } with
    | { fst := x, snd := k } => { fst := x, snd := fun y => corec construct.automaton (k y) }
⊢ ∃ node_1 k₁ k₂_1,
    destruct x = { fst := node_1, snd := k₁ } ∧
      { fst := node, snd := k₂ } = { fst := node_1, snd := k₂_1 } ∧
        ∀ (z : B C i node_1), R (N C i node_1 z) (k₁ z) (k₂_1 z)

State before:
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 =
    match construct.automaton i { fst := node, snd := k₂ } with
    | { fst := x, snd := k } => { fst := x, snd := fun y => corec construct.automaton (k y) }
⊢ ∃ node_1 k₁ k₂_1,
    destruct x = { fst := node_1, snd := k₁ } ∧
      { fst := node, snd := k₂ } = { fst := node_1, snd := k₂_1 } ∧
        ∀ (z : B C i node_1), R (N C i node_1 z) (k₁ z) (k₂_1 z)
Tactic:
simp only [construct.automaton, Map] at h₀
State after:
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)) }
⊢ ∃ node_1 k₁ k₂_1,
    destruct x = { fst := node_1, snd := k₁ } ∧
      { fst := node, snd := k₂ } = { fst := node_1, snd := k₂_1 } ∧
        ∀ (z : B C i node_1), R (N C i node_1 z) (k₁ z) (k₂_1 z)

State before:
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)) }
⊢ ∃ node_1 k₁ k₂_1,
    destruct x = { fst := node_1, snd := k₁ } ∧
      { fst := node, snd := k₂ } = { fst := node_1, snd := k₂_1 } ∧
        ∀ (z : B C i node_1), R (N C i node_1 z) (k₁ z) (k₂_1 z)
Tactic:
exists node
State after:
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)) }
⊢ ∃ k₁ k₂_1,
    destruct x = { fst := node, snd := k₁ } ∧
      { fst := node, snd := k₂ } = { fst := node, snd := k₂_1 } ∧ ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂_1 z)

State before:
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)) }
⊢ ∃ k₁ k₂_1,
    destruct x = { fst := node, snd := k₁ } ∧
      { fst := node, snd := k₂ } = { fst := node, snd := k₂_1 } ∧ ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂_1 z)
Tactic:
exists λ (x:B C i node) => construct <| destruct <| k₂ x
State after:
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)) }
⊢ ∃ k₂_1,
    destruct x = { fst := node, snd := fun x => construct (destruct (k₂ x)) } ∧
      { fst := node, snd := k₂ } = { fst := node, snd := k₂_1 } ∧
        ∀ (z : B C i node), R (N C i node z) ((fun x => construct (destruct (k₂ x))) z) (k₂_1 z)

State before:
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)) }
⊢ ∃ k₂_1,
    destruct x = { fst := node, snd := fun x => construct (destruct (k₂ x)) } ∧
      { fst := node, snd := k₂ } = { fst := node, snd := k₂_1 } ∧
        ∀ (z : B C i node), R (N C i node z) ((fun x => construct (destruct (k₂ x))) z) (k₂_1 z)
Tactic:
exists k₂
State after:
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)) }
⊢ destruct x = { fst := node, snd := fun x => construct (destruct (k₂ x)) } ∧
    { fst := node, snd := k₂ } = { fst := node, snd := k₂ } ∧
      ∀ (z : B C i node), R (N C i node z) ((fun x => construct (destruct (k₂ x))) z) (k₂ z)

State before:
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)) }
⊢ destruct x = { fst := node, snd := fun x => construct (destruct (k₂ x)) } ∧
    { fst := node, snd := k₂ } = { fst := node, snd := k₂ } ∧
      ∀ (z : B C i node), R (N C i node z) ((fun x => construct (destruct (k₂ x))) z) (k₂ z)
Tactic:
constructor
State after:
case left
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)) }
⊢ destruct x = { fst := node, snd := fun x => construct (destruct (k₂ x)) }

case 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)) }
⊢ { fst := node, snd := k₂ } = { fst := node, snd := k₂ } ∧
    ∀ (z : B C i node), R (N C i node z) ((fun x => construct (destruct (k₂ x))) z) (k₂ z)

State before:
case left
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)) }
⊢ destruct x = { fst := node, snd := fun x => construct (destruct (k₂ x)) }

case 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)) }
⊢ { fst := node, snd := k₂ } = { fst := node, snd := k₂ } ∧
    ∀ (z : B C i node), R (N C i node z) ((fun x => construct (destruct (k₂ x))) z) (k₂ z)
Tactic:
. exact h₀
State after:
case 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)) }
⊢ { fst := node, snd := k₂ } = { fst := node, snd := k₂ } ∧
    ∀ (z : B C i node), R (N C i node z) ((fun x => construct (destruct (k₂ x))) z) (k₂ z)

State before:
case 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)) }
⊢ { fst := node, snd := k₂ } = { fst := node, snd := k₂ } ∧
    ∀ (z : B C i node), R (N C i node z) ((fun x => construct (destruct (k₂ x))) z) (k₂ z)
Tactic:
. constructor
  . rfl
  . intro i
    rfl
State after:
no goals

State before:
case left
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)) }
⊢ destruct x = { fst := node, snd := fun x => construct (destruct (k₂ x)) }
Tactic:
exact h₀
State after:
no goals

State before:
case 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)) }
⊢ { fst := node, snd := k₂ } = { fst := node, snd := k₂ } ∧
    ∀ (z : B C i node), R (N C i node z) ((fun x => construct (destruct (k₂ x))) z) (k₂ z)
Tactic:
constructor
State after:
case right.left
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)) }
⊢ { fst := node, snd := k₂ } = { fst := node, snd := k₂ }

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)

State before:
case right.left
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)) }
⊢ { fst := node, snd := k₂ } = { fst := node, snd := k₂ }

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)
Tactic:
. rfl
State after:
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)

State before:
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)
Tactic:
. intro i
  rfl
State after:
no goals

State before:
case right.left
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)) }
⊢ { fst := node, snd := k₂ } = { fst := node, snd := k₂ }
Tactic:
rfl
State after:
no goals

State before:
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)
Tactic:
intro i
State after:
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)

State before:
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)
Tactic:
rfl
State after:
no goals

State before:
case a
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)
⊢ R i (construct (destruct x)) x
Tactic:
rfl
State after:
no goals