n✝ : ZFSet
x : PSet
x✝ : Quotient.mk setoid x ∈ omega
n : ℕ
h : PSet.Equiv x (Func PSet.omega { down := n })
⊢ insert (mk (Func PSet.omega { down := n })) (mk (Func PSet.omega { down := n })) =
    insert (mk (ofNat n)) (mk (ofNat n))
n✝ : ZFSet
x : PSet
x✝ : Quotient.mk setoid x ∈ omega
n : ℕ
h : PSet.Equiv x (Func PSet.omega { down := n })
⊢ insert (mk x) (mk x) = insert (mk (ofNat n)) (mk (ofNat n))
rw [ZFSet.sound h]
no goals
n✝ : ZFSet
x : PSet
x✝ : Quotient.mk setoid x ∈ omega
n : ℕ
h : PSet.Equiv x (Func PSet.omega { down := n })
⊢ insert (mk (Func PSet.omega { down := n })) (mk (Func PSet.omega { down := n })) =
    insert (mk (ofNat n)) (mk (ofNat n))
rfl