no goals
p : ZFSet → Prop
x y✝ : ZFSet
x✝¹ y : PSet
α : Type u
A : α → PSet
x✝ : Quotient.mk setoid y ∈ ZFSet.sep p (Quotient.mk setoid (PSet.mk α A))
a : Type (PSet.mk α A)
pa : (fun y => p (mk y)) (Func (PSet.mk α A) a)
h :
  PSet.Equiv y
    (Func
      ↑(Resp.f
          { val := PSet.sep fun y => p (mk y),
            property :=
              (_ :
                ∀ (x x_1 : PSet),
                  PSet.Equiv x x_1 → Arity.Equiv (PSet.sep (fun y => p (mk y)) x) (PSet.sep (fun y => p (mk y)) x_1)) }
          (PSet.mk α A))
      { val := a, property := pa })
⊢ p (Quotient.mk setoid y)
rwa [@Quotient.sound PSet _ _ _ h]
p : ZFSet → Prop
x y✝ : ZFSet
x✝¹ y : PSet
α : Type u
A : α → PSet
x✝ : Quotient.mk setoid y ∈ Quotient.mk setoid (PSet.mk α A) ∧ p (Quotient.mk setoid y)
a : Type (PSet.mk α A)
h : PSet.Equiv y (A a)
pa : p (Quotient.mk setoid y)
⊢ p (mk (Func (PSet.mk α A) a))
p : ZFSet → Prop
x y✝ : ZFSet
x✝¹ y : PSet
α : Type u
A : α → PSet
x✝ : Quotient.mk setoid y ∈ Quotient.mk setoid (PSet.mk α A) ∧ p (Quotient.mk setoid y)
a : Type (PSet.mk α A)
h : PSet.Equiv y (Func (PSet.mk α A) a)
pa : p (Quotient.mk setoid y)
⊢ (fun y => p (mk y)) (Func (PSet.mk α A) a)
rw [mk_func] at h
no goals
p : ZFSet → Prop
x y✝ : ZFSet
x✝¹ y : PSet
α : Type u
A : α → PSet
x✝ : Quotient.mk setoid y ∈ Quotient.mk setoid (PSet.mk α A) ∧ p (Quotient.mk setoid y)
a : Type (PSet.mk α A)
h : PSet.Equiv y (A a)
pa : p (Quotient.mk setoid y)
⊢ p (mk (Func (PSet.mk α A) a))
rwa [mk_func, ← ZFSet.sound h]