Stmt = Set

data _∧_ (P Q : Stmt) : Stmt where
  ⟨_,_⟩ : P → Q → P ∧ Q

data _∨_ (P Q : Stmt) : Stmt where
  inl : P → P ∨ Q
  inr : Q → P ∨ Q

data ⊥ : Stmt where

¬_ : Stmt → Stmt
¬ P = P → ⊥

module _ (Ω : Set) where
  Set' = Ω → Stmt

  _⊆_ : (A B : Set') → Stmt
  A ⊆ B = {x : Ω} → A x → B x
  infix 9 _⊆_

  _-_ : (A B : Set') → Set'
  (A - B) x = A x ∧ (¬ B x)

  _∪_ : (A B : Set') → Set'
  (A ∪ B) x = A x ∨ B x

  ∅ : Set'
  ∅ x = ⊥

  _=ₛₑₜ_ : Set' → Set' → Set
  A =ₛₑₜ B = (A ⊆ B) ∧ (B ⊆ A)
  infix 9 _=ₛₑₜ_

  module _ {A B C : Set'} where
    thm₁ : A ⊆ B → (A - C) ⊆ (B - C)
    thm₁ f ⟨ a , nc ⟩ = {!!}

    thm₂ : (A ∪ B) - C =ₛₑₜ (A - C) ∪ (B - C)
    thm₂ = ⟨ ABC-⊆ , ABC-⊇ ⟩
      where
        ABC-⊆ : (A ∪ B) - C ⊆ (A - C) ∪ (B - C)
        ABC-⊆ = {!!}
        ABC-⊇ : (A - C) ∪ (B - C) ⊆ (A ∪ B) - C
        ABC-⊇ = {!!}