rfl
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)
no goals