gistfile1.txt

module TAMO where

open import Relation.Binary.Core

data Bool : Set where
  true  : Bool
  false : Bool

data False : Set where
record True : Set where

isTrue : Bool → Set
isTrue true  = True
isTrue false = False

lem-isTrue : {p : Bool} → p ≡ true → isTrue p
lem-isTrue refl = _

lem-p≡true : (p : Bool) → isTrue p → p ≡ true
lem-p≡true true True = refl
lem-p≡true false ()