false = t
true  = t t

triage = (\a b c : t (t a b) c)

matchBool = (\ot of : triage
  of
  (\_ : ot)
  (\_ _ : ot)
)

not_TC?     = t (t (t t) (t t t)) (t t (t t t))
not_Lambda? = matchBool false true

areEqual? = equal not_TC not_Lambda

true_TC?  = not_TC false
false_TC? = not_TC true

true_Lambda?  = not_Lambda false
false_Lambda? = not_Lambda true

areTrueEqual?  = equal true_TC  true_Lambda
areFalseEqual? = equal false_TC false_Lambda