use tauto_cong;

sym qu;

fn qu_def : true -> qu'(a) == ~a {
    axiom qu_def : true -> qu'(a) == ~a;
    x : true;
    let r = qu_def(x) : qu'(a) == ~a;
    return r;
}

fn qu_tauto_cong : true -> tauto_cong'(qu') {
    axiom qu_tauto_cong : true -> tauto_cong'(qu');
    x : true;
    let r = qu_tauto_cong(x) : tauto_cong'(qu');
    return r;
}

fn qu_in_arg : ~a & (a == b)^true  ->  ~b {
    use fst;
    use pow_transitivity;
    use qu_def;
    use qu_tauto_cong;
    use snd;
    use tauto_cong_to;
    use triv;

    x : ~a;
    y : (a == b)^true;

    let x2 = triv(qu_def) : qu'(a) == ~a;
    let x3 = snd(x2) : ~a => qu'(a);
    let x4 = triv(qu_tauto_cong) : tauto_cong'(qu');
    let x5 = tauto_cong_to(x4) :
        sym(f, all((a == b)^true -> f'(a) == f'(b)))(qu');
    let x6 = x5() : (a == b)^true -> qu'(a) == qu'(b);
    let x7 = x6(y) : qu'(a) == qu'(b);
    let x8 = fst(x7) : qu'(a) => qu'(b);
    let x9 = x3(x) : qu'(a);
    let x10 = x8(x9) : qu'(b);
    let x11 = triv(qu_def) : qu'(b) == ~b;
    let x12 = fst(x11) : qu'(b) => ~b;
    let r = x12(x10) : ~b;
    return r;
}

fn qu_to_q : ~a  ->  a ~~ a {
    x : ~a;
    use std::refl;
    let y = refl() : a => a;
    let y2 = refl(y, y) : a == a;
    use q_from;
    let r = q_from(y2, x, x) : a ~~ a;
    return r;
}

fn q_to_qu : a ~~ a  ->  ~a {
    x : a ~~ a;
    use q_to;
    let y = q_to(x) : (a == a) & ~a & ~a;
    use std::snd;
    let y2 = snd(y) : ~a & ~a;
    let r = snd(y2) : ~a;
    return r;
}

fn eq_qu_q : true  ->  ~a == (a ~~ a) {
    use q_to_qu;
    use qu_to_q;
    use refl;

    x : true;

    let r = refl(qu_to_q, q_to_qu) : (~a == (a ~~ a));
    return r;
}

fn eq_q_qu : true  ->  (a ~~ a) == ~a {
    use eq_symmetry;
    use eq_qu_q;

    x : true;

    let y = eq_qu_q(x) : ~a == (a ~~ a);
    let r = eq_symmetry(y) : (a ~~ a) == ~a;
    return r;
}

fn nqu_to_sesh : !~a  ->  !(a ~~ a) {
    x: !~a;
    use q_to_qu;
    use std::modus_tollens;
    let y = modus_tollens(q_to_qu) : !~a => !(a ~~ a);
    let r = y(x) : !(a ~~ a);
    return r;
}

fn sd_to_qu : sd(a, a)  ->  ~a {
    use sd_to_q;
    use q_to_qu;

    x : sd(a, a);

    let x2 = sd_to_q(x) : a ~~ a;
    let r = q_to_qu(x2) : ~a;
    return r;
}

fn nqu_to_nsd : !~a  ->  !sd(a, a) {
    use modus_tollens;
    use sd_to_qu;

    x : !~a;

    let x2 = modus_tollens(sd_to_qu) : !~a => !sd(a, a);
    let r = x2(x) : !sd(a, a);
    return r;
}

fn qu_inv_to_nqu : ~!a  ->  !~a {
    axiom qu_inv_to_nqu : ~!a -> !~a;
    x : ~!a;
    let r = qu_inv_to_nqu(x) : !~a;
    return r;
}

fn nqu_to_qu_inv : !~a  ->  ~!a {
    axiom nqu_to_qu_inv : !~a -> ~!a;
    x : !~a;
    let r = nqu_to_qu_inv(x) : ~!a;
    return r;
}

fn qu_eq_inv : true  ->  (~!a == !~a) {
    use nqu_to_qu_inv;
    use qu_inv_to_nqu;
    use refl;

    let x1 = qu_inv_to_nqu() : ~!a => !~a;
    let x2 = nqu_to_qu_inv() : !~a => ~!a;
    let r = refl(x1, x2) : ~!a == !~a;
    return r;
}

fn tauto_qu_true_to_qu : a^true & ~true  ->  ~a {
    use tauto_to_tauto_eq_true;
    use tauto_eq_symmetry;
    use qu_in_arg;

    x : a^true;
    y : ~true;

    let x2 = tauto_to_tauto_eq_true(x) : (a == true)^true;
    let x3 = tauto_eq_symmetry(x2) : (true == a)^true;
    let r = qu_in_arg(y, x3) : ~a;
    return r;
}

fn qu_qu_true_tauto_excm_to_tauto : ~a & ~true & excm(a)^true  ->  a^true {
    use qu_inv_to_nqu;
    use refl;
    use tauto_excm_to_or;
    use tauto_qu_true_to_qu;

    x : ~a;
    y : ~true;
    z : excm(a)^true;

    let z2 = tauto_excm_to_or(z) : a^true | (!a)^true;
    let f = refl() : a^true => a^true;
    lam g : (!a)^true => a^true {
        w : (!a)^true;

        let w2 = tauto_qu_true_to_qu(w, y) : ~!a;
        let w3 = qu_inv_to_nqu(w2) : !~a;
        let w4 = w3(x) : false;
        let r = match w4 : a^true;
        return r;
    }
    let r = match z2 (f, g) : a^true;
    return r;
}

fn qu_true_tauto_excm_to_eq_tauto_qu : ~true & excm(a)^true  ->  (a^true == ~a) {
    use qu_qu_true_tauto_excm_to_tauto;
    use refl;
    use tauto_qu_true_to_qu;

    x : ~true;
    y : excm(a)^true;

    lam f : a^true => ~a {
        z : a^true;

        let r = tauto_qu_true_to_qu(z, x) : ~a;
        return r;
    }
    lam g : ~a => a^true {
        z : ~a;

        let r = qu_qu_true_tauto_excm_to_tauto(z, x, y) : a^true;
        return r;
    }
    let r = refl(f, g) : a^true == ~a;
    return r;
}