use z;
use unsafe;

sym type;

fn ty_lift : unsafe' -> (a : x) -> (a : (a : x)) {
    axiom ty_lift : unsafe' -> (a : x) -> (a : (a : x));
    x : unsafe';
    let r = ty_lift(x) : (a : x) -> (a : (a : x));
    return r;
}

fn ty_eq_left : a == b  ->  (a : c) == (b : c) {
    axiom ty_eq_left : a == b -> (a : c) == (b : c);
    x : a == b;
    let r = ty_eq_left(x) : (a : c) == (b : c);
    return r;
}

fn ty_eq_right : a == b  ->  (c : a) == (c : b) {
    axiom ty_eq_right : a == b -> (c : a) == (c : b);
    x : a == b;
    let r = ty_eq_right(x) : (c : a) == (c : b);
    return r;
}

fn ty_app : (f : a => b) & (a2 : a) -> (f(a2) : b) {
    axiom ty_app : (f : a => b) & (a2 : a) -> (f(a2) : b);
    x : (f : a => b) & (a2 : a);
    let r = ty_app(x) : (f(a2) : b);
    return r;
}

fn ty_app2 : (f : a => b => c) & (a2 : a) & (b2 : b) -> (f(a2, b2) : c) {
    x : (f : a => b => c);
    y : (a2 : a);
    z : (b2 : b);
    use ty_app;
    let x2 = ty_app(x, y) : (f(a2) : b => c);
    let r = ty_app(x2, z) : (f(a2, b2) : c);
    return r;
}

fn ty_uniq : !(a == b) & ((c : a) == (c : b)) -> false {
    axiom ty_uniq : !(a == b) & ((c : a) == (c : b)) -> false;
    x : !(a == b) & ((c : a) == (c : b));
    let r = ty_uniq(x) : false;
    return r;
}

/// Make symbolic distinct types non-equal.
fn ty_sd_to_neq : sd(a, b) & (a : type'(z')) & (b : type'(z')) -> !(a == b) {
    axiom ty_sd_to_neq : sd(a, b) & (a : type'(z')) & (b : type'(z')) -> !(a == b);
    x : sd(a, b) & (a : type'(z')) & (b : type'(z'));
    let r = ty_sd_to_neq(x) : !(a == b);
    return r;
}

fn ty_fun : (a : at) & (b : bt) -> ((a => b) : at => bt) {
    axiom ty_fun : (a : at) & (b : bt) -> ((a => b) : at => bt);
    x : (a : at) & (b : bt);
    let r = ty_fun(x) : ((a => b) : at => bt);
    return r;
}

fn ty_fun_ty : true -> (type'(a) => type'(b) : type'(z')) {
    axiom ty_fun_ty : true -> (type'(a) => type'(b) : type'(z'));
    x : true;
    let r = ty_fun_ty(x) : (type'(a) => type'(b) : type'(z'));
    return r;
}

fn ty_in_left_arg : (a : b) & (a == c) -> (c : b) {
    use ty_eq_left;
    use fst;
    
    x : (a : b);
    y : a == c;
    
    let x2 = ty_eq_left(y) : (a : b) == (c : b);
    let x3 = fst(x2) : (a : b) => (c : b);
    let r = x3(x) : (c : b);
    return r;
}

fn ty_in_right_arg : (a : b) & (b == c) -> (a : c) {
    use ty_eq_right;
    use fst;
    
    x : (a : b);
    y : b == c;
    
    let x2 = ty_eq_right(y) : (a : b) == (a : c);
    let x3 = fst(x2) : (a : b) => (a : c);
    let r = x3(x) : (a : c);
    return r;
}

fn ty_judgement : (b : type'(n))  ->  ((a : b) : type'(n)) {
    axiom ty_judgement : (b : type'(n)) -> ((a : b) : type'(n));
    x : (b : type'(n));
    let r = ty_judgement(x) : ((a : b) : type'(n));
    return r;
}

fn ty_tup_type : true -> ((type'(n), type'(m)) : type'(z')) {
    axiom ty_tup_type : true -> ((type'(n), type'(m)) : type'(z'));
    x : true;
    let r = ty_tup_type(x) : ((type'(n), type'(m)) : type'(z'));
    return r;
}

fn ty_transitivity : (a : b) & (b : c)  ->  (a : c) {
    axiom ty_transitivity : (a : b) & (b : c) -> (a : c);
    x1 : (a : b);
    x2 : (b : c);
    let r = ty_transitivity(x1, x2) : (a : c);
    return r;
}

fn ty_tup_ty : (a : x) & (b : y)  ->  ((a, b) : (x, y)) {
    axiom ty_tup_ty : (a : x) & (b : y) -> ((a, b) : (x, y));
    x1 : (a : x);
    x2 : (b : y);
    let r = ty_tup_ty(x1, x2) : ((a, b) : (x, y));
    return r;
}