namespace latin:/

fixmeta latin:/?SFOLEQ

theory Booleans =
  bool: tp
  
  tt: tm bool
  ff: tm bool

  if: {S} tm bool ⟶ tm S ⟶ tm S ⟶ tm S# if 2 then 3 else 4 prec 50

  bool_tnd : ⊦ ∀[b] b≐tt ∨ b≐ff
  bool_nontrivial : ⊦ ¬ tt≐ff
  
  if_tt : {s,x,y:tm s} ⊦ if tt then x else y ≐ x
  if_ff : {s,x,y:tm s} ⊦ if ff then x else y ≐ y