/// Type of propositions used by special operators, such as `sd`.
/// This is needed to specify congruence.
sym prop;
/// Unsafe symbol, used to guard a subset of some logic which is not entirely safe.
/// This is different from `unsafe return`.
/// To temporary allow unsafety, one can declare `axiom u : unsafe';`.
sym unsafe;

fn refl : a -> a {
    x : a;

    return x;
}

fn pow_tr : a -> true {
    let r = () : true;
    return r;
}

fn curry : (a & b) => c  ->  (a => b => c) {
    x : (a & b) => c;
    lam f : a => b => c {
        y : a;
        lam g : b => c {
            z : b;
            let r = x(y, z) : c;
            return r;
        }
        return g;
    }
    return f;
}

fn uncurry : (a => b => c) -> (a & b) => c {
    x : a => b => c;
    lam f : (a & b) => c {
        x2 : a;
        x3 : b;
        let x4 = x(x2) : b => c;
        let x5 = x4(x3) : c;
        return x5;
    }
    return f;
}

fn modus_ponens : a & (a => b) -> b {
    x : a;
    y : a => b;

    let z = y(x) : b;
    return z;
}

fn unify : (a | b) & ((a => c) & (b => c))  ->  c {
    x : (a | b);
    l : a => c;
    r : b => c;
    let y = match x (l, r) : c;
    return y;
}

fn all_pow_absurd : all(a -> b) -> c {
    x : all(a -> b);
    let y = () : true;
    let z = x(y) : c;
    return z;
}