fn sym_fun_eq : true -> sym(a, f(a')) == f {
    axiom sym_fun_eq : true -> sym(a, f(a')) == f;
    x : true;
    let r = sym_fun_eq(x) : sym(a, f(a')) == f;
    return r;
}

fn sym_transitivity : sym(a, b) & (b => c)^(sym a) -> sym(a, c) {
    axiom sym_transitivity : sym(a, b) & (b => c)^(sym a) -> sym(a, c);
    x : sym(a, b);
    y : (b => c)^(sym a);
    let r = sym_transitivity(x, y) : sym(a, c);
    return r;    
}

fn sym_transport : sym(a, b) & (b == c)^(sym a) -> sym(a, c) {
    use fst;
    use pow_transitivity;
    use sym_transitivity;

    x : sym(a, b);
    y : (b == c)^(sym a);

    let z = fst() : (b => c)^(b == c);
    let y2 = pow_transitivity(y, z) : (b => c)^(sym a);
    let r = sym_transitivity(x, y2) : sym(a, c);
    return r;
}

fn sym_eq : (a == b)^(sym c) -> sym(c, a) == sym(c, b) {
    use eq_symmetry;
    use pow_transitivity;
    use refl;
    use sym_transport;

    x : (a == b)^(sym c);

    let x2 = pow_transitivity(x, eq_symmetry) : (b == a)^(sym c);
    lam f : sym(c, a) => sym(c, b) {
        y : sym(c, a);
        let r = sym_transport(y, x) : sym(c, b);
        return r;
    }
    lam g : sym(c, b) => sym(c, a) {
        y : sym(c, b);
        let r = sym_transport(y, x2) : sym(c, a);
        return r;
    }
    let r = refl(f, g) : sym(c, a) == sym(c, b);
    return r;
}

use cong;

fn sym_cong_eq : cong'(sym(c, a)) & (a == b)^(sym c) -> sym(c, a)(x) == sym(c, b)(x) {
    use sym_eq;
    use cong_eq;
    use cong_fun_eq;
    use eq_to_right;

    y : cong'(sym(c, a));
    x : (a == b)^(sym c);

    let x2 = sym_eq(x) : sym(c, a) == sym(c, b);
    let x3 = cong_eq(x2) : cong'(sym(c, a)) == cong'(sym(c, b));
    let y2 = eq_to_right(x3, y) : cong'(sym(c, b));
    let r = cong_fun_eq(y, y2, x2) : sym(c, a)(x) == sym(c, b)(x);
    unsafe return r;
}

fn sym_all_pow_absurd : all(a -> b) -> false {
    x : all(a -> b);
    let x2 = x() : a -> b;
    let x3 = x() : (a -> b) -> false;
    let r = x3(x2) : false;
    return r;
}

fn sym_absurd : a & sym(a, all(a' -> b))(a) -> false {
    x : a;
    y : sym(a, all(a' -> b))(a);
    let y2 = y() : a -> false;
    let r = y2(x) : false;
    return r;
}

fn sym_eq_refl : sym a  ->  a' == a' {
    sym a;
    use eq_refl;
    use triv;
    let r = triv(eq_refl) : a' == a';
    return r;
}

fn sym_from : sym(a, a')(a) -> a {
    x : sym(a, a')(a);
    let r = x() : a;
    return r;
}

fn sym_unwrap : sym(a, b)(a) -> b {
    x : sym(a, b)(a);
    let r = x() : b;
    return r;
}

fn sym_to_all : a -> sym(a, all(a'))(a) {
    x : a;
    let r = x() : sym(a, all(a'))(a);
    unsafe return r;
}

fn sym_from_all : sym(a, all(a'))(a) -> a {
    x : sym(a, all(a'))(a);
    let r = x() : a;
    return r;
}

fn sym_all_conv : sym(a, all(a'))(a) -> sym(b, all(b'))(a) {
    x : sym(a, all(a'))(a);
    let r = x() : sym(b, all(b'))(a);
    unsafe return r;
}

fn sym_pow_to_pow_tauto : sym(f, a^b)(f) -> sym(f, a^(b^true))(f) {
    x : sym(f, a^b)(f);
    let x2 = x() : a^b;
    use pow_to_pow_tauto;
    let x3 = pow_to_pow_tauto(x2) : a^(b^true);
    let r = x3() : sym(f, a^(b^true))(f);
    unsafe return r;
}

fn sym_pow_lift : a^b -> (sym(a, all(a'))(a))^(sym(b, all(b'))(b)) {
    use sym_to_all;
    use sym_from_all;
    use pow_transitivity;

    x : a^b;

    let f = sym_from_all() : sym(b, all(b'))(b) -> b;
    let x2 = pow_transitivity(f, x) : sym(b, all(b'))(b) -> a;
    let g = sym_to_all() : a -> sym(a, all(a'))(a);
    let r = pow_transitivity(x2, g) : sym(b, all(b'))(b) -> sym(a, all(a'))(a);
    unsafe return r;
}