pub fn adjunction(
f: fn(fn(a) -> b) -> NotNot(b, c),
) -> NotNot(b, fn(fn(c) -> b) -> NotNot(b, a))
pub fn bind(
c: NotNot(a, b),
f: fn(b) -> NotNot(a, c),
) -> NotNot(a, c)
pub fn callcc(f: fn(fn(a) -> b) -> a) -> NotNot(b, a)
pub fn co(
f: fn(fn(a) -> b) -> NotNot(b, c),
rest: fn(Result(c, a)) -> NotNot(b, d),
) -> NotNot(b, d)
pub fn coexponential_to_function(
c: fn(#(a, fn(b) -> c)) -> c,
) -> NotNot(c, fn(a) -> NotNot(c, b))
pub fn contramap(
not_b: fn(a) -> b,
f: fn(c) -> NotNot(b, a),
) -> NotNot(b, fn(c) -> b)
pub fn de_morgan_1(
x: fn(Result(a, b)) -> c,
) -> NotNot(c, #(fn(b) -> c, fn(a) -> c))
pub fn de_morgan_2(
x: #(fn(a) -> b, fn(c) -> b),
) -> NotNot(b, fn(Result(c, a)) -> b)
pub fn de_morgan_3(
x: fn(#(a, b)) -> c,
) -> NotNot(c, Result(fn(b) -> c, fn(a) -> c))
pub fn de_morgan_4(
x: Result(fn(a) -> b, fn(c) -> b),
) -> NotNot(b, fn(#(c, a)) -> b)
pub fn disjunctive_syllogism(
e: NotNot(a, Result(b, c)),
not_a: fn(c) -> a,
) -> NotNot(a, b)
pub fn do(c: NotNot(a, b), f: fn(b) -> c) -> NotNot(a, c)
pub fn double_negate(a: a) -> NotNot(b, fn(fn(a) -> b) -> b)
pub fn double_negation_elimination(
not_not_a: fn(fn(a) -> b) -> b,
) -> NotNot(b, a)
pub fn excluded_middle() -> NotNot(a, Result(fn(b) -> a, b))
pub fn function_to_coexponential(
f: fn(a) -> NotNot(b, c),
) -> NotNot(b, fn(#(a, fn(c) -> b)) -> b)
pub fn implies(
f: fn(a) -> NotNot(b, c),
) -> NotNot(b, Result(c, fn(a) -> b))
pub fn join(a: NotNot(a, NotNot(a, b))) -> NotNot(a, b)
pub fn modus_ponens(
f: Result(a, fn(b) -> c),
a: b,
) -> NotNot(c, a)
pub fn pierces_law(
f: fn(fn(a) -> NotNot(b, c)) -> NotNot(b, a),
) -> NotNot(b, a)
pub fn throw(a: a, not_a: fn(a) -> b) -> NotNot(b, c)
pub fn wrap(a: a) -> NotNot(b, a)