exact equality_def.mpr $ Set.eq_of_subset_of_subset
  (by intro p hp; exact h p hp)
  (by
    intro p;
    contrapose;
    intro hp;
    apply iff_mem_neg.mp;
    apply h;
    apply iff_mem_neg.mpr hp;
  )
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
h : ∀ p ∈ Ω₁.theory, p ∈ Ω₂.theory
⊢ Ω₁ = Ω₂
no goals