use cong;
use prop;

sym prop_and;

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

fn and_sym_def : true -> prop_and' == sym(a, sym(b, a' & b')) {
    axiom and_sym_def : true -> prop_and' == sym(a, sym(b, a' & b'));
    x : true;
    let r = and_sym_def(x) : prop_and' == sym(a, sym(b, a' & b'));
    return r;
}

fn and_def : true -> prop_and'(a, b) == (a & b) {
    use and_cong;
    use and_sym_def;
    use and_ty;
    use cong_fun_bin_eq;
    use cong_fun_eq;
    use cong_in_arg;

    x : true;

    let y2 = and_cong(x) : cong'(prop_and');
    let y3 = and_sym_def(x) : prop_and' == sym(a, sym(b, a' & b'));
    let y4 = cong_in_arg(y2, y3) : cong'(sym(a, sym(b, a' & b')));
    let y5 = and_ty(x) : (prop_and' : prop' => prop' => prop');
    let y6 = cong_fun_bin_eq(y2, y4, y5, y3) :
        prop_and'(a, b) == sym(a, sym(b, a' & b'))(a, b);
    let r = y6() : prop_and'(a, b) == (a & b);
    return r;
}

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

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

    lam f : b => (a & b) {
        x2 : b;

        use refl;
        let x3 = refl(x, x2) : (a & b);
        return x3;
    }
    return f;
}

fn and_symmetry : a & b -> b & a {
    use fst;
    use snd;

    x : a & b;
    let y = fst(x) : a;
    let z = snd(x) : b;

    use refl;
    let r = refl(z, y) : (b & a);
    return r;
}

fn and_transitivity : (a & b) & (b & c)  ->  (a & c) {
    x : a & b;
    y : b & c;
    use fst;
    let x2 = fst(x) : a;
    use snd;
    let y2 = snd(y) : c;
    use refl;
    let r = refl(x2, y2) : a & c;
    return r;
}

fn and_associativity : true -> ((a & b) & c) == (a & (b & c)) {
    use fst;
    use snd;
    use refl;

    x : true;

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

        let y2 = fst(y) : a & b;
        let y3 = snd(y) : c;
        let y4 = fst(y2) : a;
        let y5 = snd(y2) : b;
        let y6 = refl(y5, y3) : b & c;
        let r = refl(y4, y6) : a & (b & c);
        return r;
    }
    lam g : (a & (b & c)) => ((a & b) & c) {
        y : a & (b & c);

        let y2 = fst(y) : a;
        let y3 = snd(y) : b & c;
        let y4 = fst(y3) : b;
        let y5 = snd(y3) : c;
        let y6 = refl(y2, y4) : a & b;
        let r = refl(y6, y5) : (a & b) & c;
        return r;
    }
    let r = refl(f, g) : ((a & b) & c) == (a & (b & c));
    return r;
}

fn fst : (a & b) -> a {
    x : a;
    y : b;
    return x;
}

fn snd : a & b -> b {
    x : a;
    y : b;
    return y;
}

fn and_eq_left : a == b -> (a & c) == (b & c) {
    use eq_to_left;
    use eq_to_right;
    use refl;

    x : a == b;

    lam f : (a & c) => (b & c) {
        y1 : a;
        y2 : c;

        let y3 = eq_to_right(x, y1) : b;
        let r = refl(y3, y2) : b & c;
        return r;
    }
    lam g : (b & c) => (a & c) {
        y1 : b;
        y2 : c;

        let y3 = eq_to_left(x, y1) : a;
        let r = refl(y3, y2) : a & c;
        return r;
    }
    let r = refl(f, g) : (a & c) == (b & c);
    return r;
}

fn and_eq_right : a == b -> (c & a) == (c & b) {
    use eq_to_left;
    use eq_to_right;
    use refl;

    x : a == b;

    lam f : (c & a) => (c & b) {
        y1 : c;
        y2 : a;

        let y3 = eq_to_right(x, y2) : b;
        let r = refl(y1, y3) : c & b;
        return r;
    }
    lam g : (c & b) => (c & a) {
        y1 : c;
        y2 : b;

        let y3 = eq_to_left(x, y2) : a;
        let r = refl(y1, y3) : c & a;
        return r;
    }
    let r = refl(f, g) : (c & a) == (c & b);
    return r;
}

fn and_to_eq : a & b -> a == b {
    use imply_lift;
    use refl;

    x : a;
    y : b;

    let f = imply_lift(y) : a => b;
    let g = imply_lift(x) : b => a;
    let r = refl(f, g) : a == b;
    return r;
}