Pasted

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-⊇ = {!!}