use cong;
use prop;

sym prop_imply;

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

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

fn imply_def : true -> prop_imply'(a, b) == (a => b) {
    use imply_cong;
    use imply_sym_def;
    use imply_ty;
    use cong_fun_bin_eq;
    use cong_fun_eq;
    use cong_in_arg;

    x : true;

    let y2 = imply_cong(x) : cong'(prop_imply');
    let y3 = imply_sym_def(x) : prop_imply' == sym(a, sym(b, a' => b'));
    let y4 = cong_in_arg(y2, y3) : cong'(sym(a, sym(b, a' => b')));
    let y5 = imply_ty(x) : (prop_imply' : prop' => prop' => prop');
    let y6 = cong_fun_bin_eq(y2, y4, y5, y3) :
        prop_imply'(a, b) == sym(a, sym(b, a' => b'))(a, b);
    let r = y6() : prop_imply'(a, b) == (a => b);
    return r;
}

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

fn imply_refl : true -> a => a {
    use refl;

    x : true;

    let r = refl() : a => a;
    return r;
}

fn imply_transitivity : (a => b) & (b => c) -> (a => c) {
    x : a => b;
    y : b => c;
    lam f : (a => c) {
        arg : a;
        let x2 = x(arg) : b;
        let x3 = y(x2) : c;
        return x3;
    }
    return f;
}

fn modus_tollens : (a => b)  ->  (!b => !a) {
    x : a => b;
    lam f : !b => !a {
        y : !b;
        lam g : !a {
            z : a;
            let x2 = x(z) : b;
            let r = y(x2) : false;
            return r;
        }
        return g;
    }
    return f;
}

fn rev_modus_tollens_nn : (!!a => !!b)  ->  (!b => !a) {
    x : !!a => !!b;
    use modus_tollens;
    let y = modus_tollens(x) : !!!b => !!!a;
    use not_double;
    use imply_transitivity;
    let f = not_double() : !b => !!!b;
    let y2 = imply_transitivity(f, y) : !b => !!!a;
    use not_rev_triple;
    let g = not_rev_triple() : !!!a => !a;    
    let r = imply_transitivity(y2, g) : !b => !a;
    return r;
}

fn rev_modus_tollens_excm : (!a => !b) & excm(a) & excm(b)  ->  b => a {
    use refl;

    x : !a => !b;
    y : excm(a);
    z : excm(b);

    lam f : b => a {
        x2 : b;

        let f = refl() : a => a;
        lam g : !a => a {
            x3 : !a;

            let x4 = x(x3) : !b;
            let x5 = x4(x2) : false;
            let r = match x5 : a;
            return r;
        }
        let r = match y (f, g) : a;
        return r;
    }
    return f;
}

fn imply_in_left_arg : (a => b) & (a == c)  ->  (c => b) {
    x : a => b;
    y : a == c;
    use snd;
    let y2 = snd(y) : c => a;
    use imply_transitivity;
    let r = imply_transitivity(y2, x) : c => b;
    return r;
}

fn imply_in_right_arg : (a => b) & (b == c)  ->  (a => c) {
    x : a => b;
    y : b == c;
    use fst;
    let y2 = fst(y) : b => c;
    use imply_transitivity;
    let r = imply_transitivity(x, y2) : a => c;
    return r;
}

fn imply_eq_left : (a == b)  ->   (a => c) == (b => c) {
    x : a == b;
    lam f : (a => c) => (b => c) {
        y : a => c;
        use snd;
        let x2 = snd(x) : b => a;
        use imply_transitivity;
        let r = imply_transitivity(x2, y) : b => c;
        return r;
    }
    lam g : (b => c) => (a => c) {
        y : b => c;
        use fst;
        let x2 = fst(x) : a => b;
        use imply_transitivity;
        let r = imply_transitivity(x2, y) : a => c;
        return r;
    }
    use refl;
    let r = refl(f, g) : (a => c) == (b => c);
    return r;
}

fn imply_eq_right : (a == b)  ->  (c => a) == (c => b) {
    x : a == b;
    lam f : (c => a) => (c => b) {
        y : c => a;
        lam r : c => b {
            use eq_to_right;
            z : c;
            let z2 = y(z) : a;
            let r = eq_to_right(x, z2) : b;
            return r;
        }
        return r;
    }
    lam g : (c => b) => (c => a) {
        y : c => b;
        lam r : c => a {
            use eq_to_left;
            z : c;
            let z2 = y(z) : b;
            let r = eq_to_left(x, z2) : a;
            return r;
        }
        return r;
    }
    use refl;
    let r = refl(f, g) : (c => a) == (c => b);
    return r;
}

fn imply_lift : a -> (b => a) {
    x : a;
    lam f : b => a {
        y : b;
        let r = x() : a;
        return r;
    }
    return f;
}

fn imply_excm_left_to_or : (a => b) & excm(a)  ->  (!a | b) {
    x : a => b;
    y : excm(a);
    lam f : a => (!a | b) {
        use right;

        x2 : a;

        let y2 = x(x2) : b;
        let r = right(y2) : !a | b;
        return r;
    }
    lam g : !a => (!a | b) {
        use left;

        x2 : !a;

        let r = left(x2) : !a | b;
        return r;
    }
    let r = match y (f, g) : !a | b;
    return r;
}

fn imply_excm_right_to_or : (a => b) & excm(b)  ->  (!a | b) {
    x : a => b;
    y : excm(b);
    lam f : b => (!a | b) {
        use right;

        x2 : b;

        let r = right(x2) : !a | b;
        return r;
    }
    lam g : !b => (!a | b) {
        use left;
        use modus_tollens;

        x2 : !b;

        let x3 = modus_tollens(x) : !b => !a;
        let x4 = x3(x2) : !a;
        let r = left(x4) : !a | b;
        return r;
    }
    let r = match y (f, g) : !a | b;
    return r;
}

fn imply_from_or : (!a | b)  ->  (a => b) {
    use imply_lift;

    x : !a | b;

    lam f : !a => (a => b) {
        use absurd;
        use imply_transitivity;

        y : !a;

        let y2 = absurd() : false => b;
        let r = imply_transitivity(y, y2) : a => b;
        return r;
    }
    let g = imply_lift() : b => (a => b);
    let r = match x (f, g) : a => b;
    return r;
}