/*
Excluded middle axiom `a | !a`
Formal expression `Excm'`
*/

sym Excm;

fn excm_to : Excm' -> all(a | !a) {
    axiom excm_to : Excm' -> all(a | !a);
    x : Excm';
    let r = excm_to(x) : all(a | !a);
    unsafe return r;
}

fn excm_from : all(a | !a) -> Excm' {
    axiom excm_from : all(a | !a) -> Excm';
    x : all(a | !a);
    let r = excm_from(x) : Excm';
    return r;
}

fn para_nexcm : !excm(a) -> false {
    x : !excm(a);

    lam f : !a {
        y : a;

        use left;
        let y2 = left(y) : excm(a);
        let r = x(y2) : false;
        return r; 
    }
    use right;
    let x2 = right() : !a => excm(a);
    let x3 = x2(f) : excm(a);
    let r = x(x3) : false;
    return r;
}

fn nnexcm : true -> !!excm(a) {
    use para_nexcm;
    let r = para_nexcm() : !!excm(a);
    return r;
}

fn excm_or_imply_left : excm(a)  ->  ((a => b) | (b => a)) {
    x : excm(a);

    lam f : a => ((a => b) | (b => a)) {
        use imply_lift;
        use right;
        
        z : a;

        let z2 = imply_lift(z) : b => a;
        let r = right(z2) : (a => b) | (b => a);
        return r;
    }
    lam g : !a => ((a => b) | (b => a)) {
        use absurd;
        use imply_transitivity;
        use left;

        z : !a;

        let z2 = absurd() : false => b;
        let z3 = imply_transitivity(z, z2) : a => b;
        let r = left(z3) : (a => b) | (b => a);
        return r;
    }
    let r = match x (f, g) : (a => b) | (b => a);
    return r;
}

fn excm_or_imply_right : excm(b)  ->  ((a => b) | (b => a)) {
    use excm_or_imply_left;
    use or_symmetry;

    x : excm(b);

    let x2 = excm_or_imply_left(x) : (b => a) | (a => b);
    let r = or_symmetry(x2) : (a => b) | (b => a);
    return r;
}