Theory boolSimpsContext

⊢ ∀p q r s.
    (if p then if p then q else r else s) = (if p then q else s) ∧
    (if p then q else if p then r else s) = (if p then q else s) ∧
    (if p then if ¬p then q else r else s) = (if p then r else s) ∧
    (if p then q else if ¬p then r else s) = if p then q else r

⊢ LET f (I x) = f x

⊢ v = v' ⇒ LET f v = LET f (I v')

⊢ literal_case f (I x) = f x

⊢ v = v' ⇒ literal_case f v = literal_case f (I v')