rcases merge hf hg H with ⟨k, _, hk⟩
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
a : α
x : σ
⊢ x ∈ f.merge g a ↔ x ∈ f a ∨ x ∈ g a
case intro.intro
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
a : α
x : σ
k : α →. σ
left✝ : Partrec k
hk : ∀ (a : α) (x : σ), x ∈ k a ↔ x ∈ f a ∨ x ∈ g a
⊢ x ∈ f.merge g a ↔ x ∈ f a ∨ x ∈ g a