unit.m31

require eq ;;

rule unit type
;;

rule tt : unit
;;

rule unit_ind
  ({x : unit} C type) (c : C{tt}) (a : unit)
  : C{a}
;;

rule unit_β
  ({x : unit} C type) (c : C{tt})
  : unit_ind C c tt ≡ c : C{tt}
;;

eq.add_rule unit_β ;;

rule unit_ext
  (s : unit) (t : unit)
  : s ≡ t : unit
;;

eq.add_rule unit_ext;;