def id (A : type) (x : A) : A := x

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

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

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

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