pub fn adjunction(
  f: fn(fn(a) -> b) -> Cont(b, c),
) -> Cont(b, fn(fn(c) -> b) -> Cont(b, a))

pub fn coexponential_to_function(
  c: fn(#(a, fn(b) -> c)) -> c,
) -> Cont(c, fn(a) -> Cont(c, b))

pub fn contramap(
  not_b: fn(a) -> b,
  f: fn(c) -> Cont(b, a),
) -> Cont(b, fn(c) -> b)

pub fn de_morgan_1(
  x: fn(Result(a, b)) -> c,
) -> Cont(c, #(fn(b) -> c, fn(a) -> c))

pub fn de_morgan_2(
  x: #(fn(a) -> b, fn(c) -> b),
) -> Cont(b, fn(Result(c, a)) -> b)

pub fn de_morgan_3(
  x: fn(#(a, b)) -> c,
) -> Cont(c, Result(fn(b) -> c, fn(a) -> c))

pub fn de_morgan_4(
  x: Result(fn(a) -> b, fn(c) -> b),
) -> Cont(b, fn(#(c, a)) -> b)

pub fn disjunctive_syllogism(
  e: Cont(a, Result(b, c)),
  not_a: fn(c) -> a,
) -> Cont(a, b)

pub fn double_negate(a: a) -> Cont(b, fn(fn(a) -> b) -> b)

pub fn double_negation_elimination(
  not_not_a: fn(fn(a) -> b) -> b,
) -> Cont(b, a)

pub fn excluded_middle() -> Cont(a, Result(fn(b) -> a, b))

pub fn function_to_coexponential(
  f: fn(a) -> Cont(b, c),
) -> Cont(b, fn(#(a, fn(c) -> b)) -> b)

pub fn implies(
  f: fn(a) -> Cont(b, c),
) -> Cont(b, Result(c, fn(a) -> b))

pub fn modus_ponens(f: Result(a, fn(b) -> c), a: b) -> Cont(c, a)

pub fn pierces_law(
  f: fn(fn(a) -> Cont(b, c)) -> Cont(b, a),
) -> Cont(b, a)