sym uniform;
sym theory;

fn uniform_to : uniform'(a)  ->  (a^true | false^a) {
    axiom uniform_to : uniform'(a)  ->  (a^true | false^a);
    x : uniform'(a);
    let r = uniform_to(x) : (a^true | false^a);
    return r;
}

fn uniform_from : (a^true | false^a)  ->  uniform'(a) {
    axiom uniform_from : (a^true | false^a)  ->  uniform'(a);
    x : a^true | false^a;
    let r = uniform_from(x) : uniform'(a);
    return r;
}

fn tauto_uniform_eq : true  ->  (uniform'(a) == (a^true | false^a)) {
    use refl;
    use uniform_to;
    use uniform_from;

    x : true;

    let x2 = uniform_to() : uniform'(a) => (a^true | false^a);
    let x3 = uniform_from() : (a^true | false^a) => uniform'(a);
    let r = refl(x2, x3) : uniform'(a) == (a^true | false^a);
    return r;
}

fn tauto_to_uniform : a^true  ->  uniform'(a) {
    use left;
    use uniform_from;

    x : a^true;

    let y = left(x) : a^true | false^a;
    let r = uniform_from(y) : uniform'(a);
    return r;
}

fn para_to_uniform : false^a  -> uniform'(a) {
    use right;
    use uniform_from;

    x : false^a;

    let y = right(x) : a^true | false^a;
    let r = uniform_from(y) : uniform'(a);
    return r;
}

fn theory_to_uniform : theory'(a)  ->  !uniform'(a) {
    axiom theory_to_uniform : theory'(a)  ->  !uniform'(a);
    x : theory'(a);
    let r = theory_to_uniform(x) : !uniform'(a);
    return r;
}

fn uniform_to_theory : !uniform'(a)  ->  theory'(a) {
    axiom uniform_to_theory : !uniform'(a)  ->  theory'(a);
    x : !uniform'(a);
    let r = uniform_to_theory(x) : theory'(a);
    return r;
}

fn theory_to : theory'(a)  ->  !(a^true | false^a) {
    use imply_in_left_arg;
    use tauto_uniform_eq;
    use theory_to_uniform;
    use triv;

    x : theory'(a);

    let y = theory_to_uniform(x) : !uniform'(a);
    let y2 = triv(tauto_uniform_eq) : uniform'(a) == (a^true | false^a);
    let r = imply_in_left_arg(y, y2) : !(a^true | false^a);        
    return r;
}

fn nor_tauto_para_to_theory : !(a^true | false^a)  -> theory'(a) {
    use eq_symmetry;
    use imply_in_left_arg;
    use tauto_uniform_eq;
    use triv;
    use uniform_to_theory;
    
    x : !(a^true | false^a);
    
    let x2 = triv(tauto_uniform_eq) : uniform'(a) == (a^true | false^a);
    let x3 = eq_symmetry(x2) : (a^true | false^a) == uniform'(a);
    let x4 = imply_in_left_arg(x, x3) : !uniform'(a);
    let r = uniform_to_theory(x4) : theory'(a);
    return r;
}

fn theory_to_ntauto : theory'(a)  ->  !(a^true) {
    use nleft;
    use theory_to;

    x : theory'(a);

    let y = theory_to(x) : !(a^true | false^a);
    let r = nleft(y) : !(a^true);
    return r;
}

fn theory_to_npara : theory'(a)  ->  !(false^a) {
    use nright;
    use theory_to;

    x : theory'(a);

    let y = theory_to(x) : !(a^true | false^a);
    let r = nright(y) : !(false^a);
    return r;
}

fn and_ntauto_npara_to_theory : !(a^true) & !(false^a)  ->  theory'(a) {
    use nor_tauto_para_to_theory;

    x : !(a^true);
    y : !(false^a);

    lam f : !(a^true | false^a) {
        z : a^true | false^a;
        let r = match z (x, y) : false;
        return r;
    }
    let r = nor_tauto_para_to_theory(f) : theory'(a);
    return r;
}

fn uniform_to_tauto_excm : uniform'(a)  ->  excm(a)^true {
    use uniform_to;

    x : uniform'(a);

    lam g : a^true => excm(a)^true {
        use left;
        use pow_transitivity;

        y : a^true;

        let f = pow_transitivity() : a^true & excm(a)^a -> excm(a)^true;
        let l = left() : excm(a)^a;
        let r = f(y, l) : excm(a)^true;
        return r;
    }
    lam h : false^a => excm(a)^true {
        use pow_to_imply_lift;
        use pow_transitivity;

        y : false^a;

        let x2 = pow_to_imply_lift(y) : (!a)^true;
        use right;
        let y2 = right() : excm(a)^(!a);
        let r = pow_transitivity(x2, y2) : excm(a)^true;
        return r;
    }
    let x2 = uniform_to(x) : a^true | false^a;
    let r = match x2 (g, h) : excm(a)^true;
    return r;
}

fn tauto_excm_to_uniform : excm(a)^true  ->  uniform'(a) {
    use hooo_or;
    use imply_transitivity;
    use tauto_not_to_para;
    use tauto_to_uniform;

    x : excm(a)^true;

    let x2 = hooo_or(x) : a^true | (!a)^true;
    let y = tauto_to_uniform() : a^true => uniform'(a);
    let tnp = tauto_not_to_para() : (!a)^true => false^a;
    use para_to_uniform;
    let ptu = para_to_uniform() : false^a => uniform'(a);
    let y2 = imply_transitivity(tnp, ptu) : (!a)^true => uniform'(a); 
    let r = match x2 (y, y2) : uniform'(a);
    return r;
}