substLeft :: Theorem Three
substLeft = undefined

-- | ⊢ (X ↔ Y) → (P → X ↔ P → Y)
substRight :: Theorem Three
substRight = undefined

-- | ⊢ (X ↔ Y) → (¬X ↔ ¬Y)
subs
reflect :: (Ord a, Show a) => Theorem a -> Theorem a
reflect = undefined
reflect = undefined