def not : bool -> bool :=
  \x -> bool-elim x at _ -> bool [
    true => false,
    false => true
  ]

def and : bool -> bool -> bool :=
  \x -> \y -> bool-elim x at _ -> bool [
    true => bool-elim y at _ -> bool [
      true => true,
      false => false
    ],
    false => false
  ]

def or : bool -> bool -> bool :=
  \x -> \y -> bool-elim x at _ -> bool [
    true => true,
    false => bool-elim y at _ -> bool [
      true => true,
      false => false
    ]
  ]

def xor : bool -> bool -> bool :=
  \x -> \y -> or
    (and x (not y))
	(and (not x) y)