open import Paths
open import Logic::False
open import Arith::Bool::Core

private def bool-inj Bool : Type
| true ⇒ Bool
| false ⇒ False
def t≠f (p : true = false) : False ⇒ transport bool-inj p true

def notTrue {b : Bool} (p : ¬ (b = true)) : b = false
| {true}, p ⇒ elim (p idp)
| {false}, _ ⇒ idp

def notFalse {b : Bool} (p : ¬ (b = false)) : b = true
| {false}, p ⇒ elim (p idp)
| {true}, _ ⇒ idp