simp[hk, merge_iff hf hg H]
case H
α : 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
k : α →. σ
pk : Partrec k
hk : ∀ (a : α) (x : σ), x ∈ k a ↔ x ∈ f a ∨ x ∈ g a
a✝ : α
a : σ
⊢ a ∈ k a✝ ↔ a ∈ f.merge g a✝
no goals