apply bisim R
C : Container
x : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
⊢ construct (destruct x) = x
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