use cong;
use prop;

sym prop_or;

fn or_ty : true -> (prop_or' : prop' => prop' => prop') {
    axiom or_ty : true -> (prop_or' : prop' => prop' => prop');
    x : true;
    let r = or_ty(x) : (prop_or' : prop' => prop' => prop');
    return r;
}

fn or_sym_def : true -> prop_or' == sym(a, sym(b, a' | b')) {
    axiom or_sym_def : true -> prop_or' == sym(a, sym(b, a' | b'));
    x : true;
    let r = or_sym_def(x) : prop_or' == sym(a, sym(b, a' | b'));
    return r;
}

fn or_def : true -> prop_or'(a, b) == (a | b) {
    use or_cong;
    use or_sym_def;
    use or_ty;
    use cong_fun_bin_eq;
    use cong_fun_eq;
    use cong_in_arg;

    x : true;

    let y2 = or_cong(x) : cong'(prop_or');
    let y3 = or_sym_def(x) : prop_or' == sym(a, sym(b, a' | b'));
    let y4 = cong_in_arg(y2, y3) : cong'(sym(a, sym(b, a' | b')));
    let y5 = or_ty(x) : (prop_or' : prop' => prop' => prop');
    let y6 = cong_fun_bin_eq(y2, y4, y5, y3) :
        prop_or'(a, b) == sym(a, sym(b, a' | b'))(a, b);
    let r = y6() : prop_or'(a, b) == (a | b);
    return r;
}

fn or_cong : true -> cong'(prop_or') {
    axiom or_cong : true -> cong'(prop_or');
    x : true;
    let r = or_cong(x) : cong'(prop_or');
    return r;
}

fn or_symmetry : a | b -> b | a {
    use unify;
    use left;
    use right;

    x : a | b;

    let x2 = right() : a => (b | a);
    let x3 = left() : b => (b | a);

    let x4 = unify(x, x2, x3) : (b | a);
    return x4;
}

fn or_associativity : true -> ((a | b) | c) == (a | (b | c)) {
    use left;
    use refl;
    use right;

    x : true;

    lam f : ((a | b) | c) => (a | (b | c)) {
        y : (a | b) | c;

        lam f : (a | b) => (a | (b | c)) {
            z : a | b;

            lam f : a => (a | (b | c)) {
                z2 : a;

                let r = left(z2) : a | (b | c);
                return r;
            }
            lam g : b => (a | (b | c)) {
                z2 : b;

                let z3 = left(z2) : b | c;
                let r = right(z3) : a | (b | c);
                return r;
            }
            let r = match z (f, g) : a | (b | c);
            return r;
        }
        lam g : c => (a | (b | c)) {
            z : c;

            let z2 = right(z) : b | c;
            let r = right(z2) : a | (b | c);
            return r;
        }
        let r = match y (f, g) : a | (b | c);
        return r;
    }
    lam g : (a | (b | c)) => ((a | b) | c) {
        y : a | (b | c);

        lam f : a => ((a | b) | c) {
            z : a;

            let z2 = left(z) : a | b;
            let r = left(z2) : (a | b) | c;
            return r;
        }
        lam g : (b | c) => ((a | b) | c) {
            z : b | c;

            lam f : b => ((a | b) | c) {
                z2 : b;

                let z3 = right(z2) : a | b;
                let r = left(z3) : (a | b) | c;
                return r;
            }
            let g = right() : c => ((a | b) | c);
            let r = match z (f, g) : (a | b) | c;
            return r;
        }
        let r = match y (f, g) : (a | b) | c;
        return r;
    }
    let r = refl(f, g) : ((a | b) | c) == (a | (b | c));
    return r;
}

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

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

fn nleft : !(a | b) -> !a {
    x : !(a | b);
    use left;
    use modus_tollens;
    let y = modus_tollens(left) : !(a | b) => !a;
    let r = y(x) : !a;
    return r;
}

fn nright : !(a | b) -> !b {
    x : !(a | b);
    use right;
    use modus_tollens;
    let y = modus_tollens(right) : !(a | b) => !b;
    let r = y(x) : !b;
    return r;
}

fn or_eq_left : a == b -> (a | c) == (b | c) {
    use eq_to_left;
    use eq_to_right;
    use left;
    use refl;
    use right;

    x : a == b;

    lam f : (a | c) => (b | c) {
        y : a | c;

        lam f : a => (b | c) {
            z : a;

            let z2 = eq_to_right(x, z) : b;
            let r = left(z2) : b | c;
            return r;
        }
        let g  = right() : c => (b | c);
        let r = match y (f, g) : b | c;
        return r;
    }
    lam g : (b | c) => (a | c) {
        y : b | c;

        lam f : b => (a | c) {
            z : b;

            let z2 = eq_to_left(x, z) : a;
            let r = left(z2) : a | c;
            return r;
        }
        let g = right() : c => (a | c);
        let r = match y (f, g) : a | c;
        return r;
    }
    let r = refl(f, g) : (a | c) == (b | c);
    return r;
}

fn or_eq_right : a == b -> (c | a) == (c | b) {
    use eq_to_left;
    use eq_to_right;
    use left;
    use refl;
    use right;

    x : a == b;

    lam f : (c | a) => (c | b) {
        y : c | a;

        let f = left() : c => (c | b);
        lam g : a => (c | b) {
            z : a;

            let z2 = eq_to_right(x, z) : b;
            let r = right(z2) : c | b;
            return r;
        }
        let r = match y (f, g) : c | b;
        return r;
    }
    lam g : (c | b) => (c | a) {
        y : c | b;

        let f = left() : c => (c | a);
        lam g : b => (c | a) {
            z : b;

            let z2 = eq_to_left(x, z) : a;
            let r = right(z2) : c | a;
            return r;
        }
        let r = match y (f, g) : c | a;
        return r;
    }
    let r = refl(f, g) : (c | a) == (c | b);
    return r;
}