Skolemization in Proofs
Skolemization is, rougly speaking, the practice of writing existential quantifiers as arrow types. This helps simplify our type system by eliminating existential quantifiers.
forall x:X. exists y:X. x + y == x^2
becomes
let g: X => X;
forall x:X. x + g(x) == x^2
In the Assumptions and Conclusions method of proof verification, the skolem function goes after the assumptions. This is equivalent to saying "forall universal quantifiers and some assumptions, there exists a skolem function".
let some_proof <A:Integer,B:Odd,C:Prime> (
assumption1: Property1<A,B>):
Conclusion<A,B,C> = {
let skolem1: (A,B,C) -> Integer;
//Here we will derive the conclusion
//starting from the assumptions
}