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❙
❚