fn para_to_not : false^a  ->  !a {
    x : false^a;

    lam g : !a {
        y : a;
        let r = x(y) : false;
        return r;
    }
    return g;
}

fn tauto_not_to_para : (!a)^true  ->  false^a {
    x : (!a)^true;
    fn f : a -> (!a)^true => false {
        y : a;
        lam g : (!a)^true => false {
            x : (!a)^true;
            use triv;
            let x2 = triv(x) : !a;
            let r = x2(y) : false;
            return r;
        }
        return g;
    }

    use hooo_imply;
    let y2 = hooo_imply(f) : ((!a)^true)^a => false^a;
    use pow_lift;
    let y3 = pow_lift(x) : ((!a)^true)^a;
    let r = y2(y3) : false^a;
    return r;
}

fn para_to_tauto_not : false^a  ->  (a => false)^true {
    x : false^a;
    use pow_to_imply_lift;
    let r = pow_to_imply_lift(x) : (a => false)^true;
    return r;
}

fn tauto_eq_tauto_not_para : true -> (!a)^true == false^a {
    use tauto_not_to_para;
    use para_to_tauto_not;
    use refl;
    
    x : true;
    
    let r = refl(tauto_not_to_para, para_to_tauto_not) : (!a)^true == false^a;
    return r;
}

fn tauto_imply_to_pow : (a => b)^true  ->  b^a {
    x : (a => b)^true;
    fn f : a -> (a => b)^true => b {
        y : a;
        lam g : (a => b)^true => b {
            z : (a => b)^true;
            use triv;
            let z2 = triv(z) : a => b;
            let r = z2(y) : b;
            return r;
        }
        return g;
    }
    use hooo_imply;
    let x2 = hooo_imply(f) : ((a => b)^true)^a => b^a;
    use pow_lift;
    let x3 = pow_lift(x) : ((a => b)^true)^a;
    let r = x2(x3) : b^a;
    return r;
}

fn tauto_imply_refl : true  ->  (a => a) {
    x : true;
    use refl;
    let y = refl() : a => a;
    return y;
}

fn tauto_eq_refl : true  ->  (a == a) {
    x : true;
    use refl;
    let y = refl() : a => a;
    let r = refl(y, y) : a == a;
    return r;
}

fn tauto_nnexcm : true  ->  !!excm(a) {
    x : true;
    lam f : !!excm(a) {
        y : !excm(a);
        lam g : !a {
            x2 : a;
            use left;
            let x3 = left(x2) : excm(a);
            let r = y(x3) : false;
            return r;
        }
        lam h : !!a {
            x4 : !a;
            use right;
            let x5 = right(x4) : excm(a);
            let r = y(x5) : false;
            return r;
        }
        let r = h(g) : false;
        return r;
    }
    return f;
}

fn pow_eq_to_tauto_eq : a =^= b  ->  (a == b)^true {
    x : b^a;
    y : a^b;

    use pow_to_imply_lift;
    let x2 = pow_to_imply_lift(x) : (a => b)^true;
    let y2 = pow_to_imply_lift(y) : (b => a)^true;

    use hooo_rev_and;
    let r = hooo_rev_and(x2, y2) : (a == b)^true;
    return r;
}

fn tauto_eq_to_pow_eq : (a == b)^true  ->  a =^= b {
    x : (a == b)^true;
    use refl;
    let x2 = refl() : a^a;
    use pow_in_left_arg;
    let x3 = pow_in_left_arg(x2, x) : b^a;
    use pow_in_right_arg;
    let x4 = pow_in_right_arg(x2, x) : a^b;
    let r = refl(x3, x4) : b^a & a^b;
    return r;
}

fn pow_in_left_arg : a^b & (a == c)^true  ->  c^b {
    x : a^b;
    y : (a == c)^true;

    use pow_lift;
    let y2 = pow_lift(y) : ((a == c)^true)^b;
    use hooo_rev_and;
    let y3 = hooo_rev_and(x, y2) : (a & (a == c)^true)^b;

    fn f : a & (a == c)^true  ->  c {
        x : a;
        y : (a == c)^true;

        use triv;
        let x2 = triv(y) : a == c;
        use fst;
        let x3 = fst(x2) : a => c;
        let r = x3(x) : c;
        return r;
    }

    use pow_transitivity;
    let y4 = pow_transitivity() :
        (a & (a == c)^true)^b & c^(a & (a == c)^true) -> c^b;
    let f2 = f() : a & (a == c)^true -> c;
    let r = y4(y3, f2) : c^b;
    return r;
}

fn pow_in_right_arg : a^b & (b == c)^true  ->  a^c {
    x : a^b;
    y : (b == c)^true;

    fn f : c  ->  (b == c)^true => b {
        x : c;
        lam g : (b == c)^true => b {
            y : (b == c)^true;
            use triv;
            let y2 = triv(y) : b == c;
            use snd;
            let y3 = snd(y2) : c => b;
            let r = y3(x) : b;
            return r;
        }
        return g;
    }

    use hooo_imply;
    let x2 = hooo_imply(f) : ((b == c)^true)^c => b^c;
    use pow_lift;
    let x3 = pow_lift(y) : ((b == c)^true)^c;
    let x4 = x2(x3) : b^c;
    use pow_transitivity;
    let r = pow_transitivity(x4, x) : a^c;
    return r;
}

fn not_to_not_tauto : !a  ->  !(a^true) {
    x : !a;
    lam f : !(a^true) {
        y : a^true;
        use triv;
        let y2 = triv(y) : a;
        let r = x(y2) : false;
        return r;
    }
    return f;
}

fn pow_modus_tollens : (a -> b)  ->  (!b -> !a) {
    x : a -> b;
    use pow_to_imply_lift;
    let x2 = pow_to_imply_lift(x) : (a => b)^true;
    use modus_tollens;
    use pow_transitivity;
    let f = modus_tollens() : (a => b) -> (!b => !a);
    let x3 = pow_transitivity(x2, f) : (!b => !a)^true;
    use tauto_imply_to_pow;
    let r = tauto_imply_to_pow(x3) : !b -> !a;
    return r;
}

fn pow_and_lift : a^b & c^d -> (a^b & c^d)^e {
    use pow_lift;
    use hooo_rev_and;

    x : a^b;
    y : c^d;
    let x2 = pow_lift(x) : (a^b)^e;
    let y2 = pow_lift(y) : (c^d)^e;
    let r = hooo_rev_and(x2, y2) : (a^b & c^d)^e;
    return r;
}

fn pow_or_lift : a^b | c^d -> (a^b | c^d)^e {
    use hooo_rev_or;

    x : a^b | c^d;

    lam g : a^b => (a^b)^e | (c^d)^e {
        y : a^b;
        use pow_lift;
        let y2 = pow_lift(y) : (a^b)^e;
        use left;
        let r = left(y2) : (a^b)^e | (c^d)^e;
        return r;
    }
    lam h : c^d => (a^b)^e | (c^d)^e {
        y3 : c^d;
        use pow_lift;
        let y4 = pow_lift(y3) : (c^d)^e;
        use right;
        let r = right(y4) : (a^b)^e | (c^d)^e;
        return r;
    }
    let x2 = match x (g, h) : (a^b)^e | (c^d)^e;
    let r = hooo_rev_or(x2) : (a^b | c^d)^e;
    return r;
}

fn pow_to_pow_tauto : a^b -> a^(b^true) {
    use pow_transitivity;
    use triv;

    x : a^b;

    let x2 = triv() : b^true -> b;
    let r = pow_transitivity(x2, x) : a^(b^true);
    return r;
}

fn tauto_eq_to_left : (a == b)^true & b -> a {
    use triv;
    use eq_to_left;

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

    let x2 = triv(x) : a == b;
    let r = eq_to_left(x2, y) : a;
    return r;
}

fn tauto_eq_to_right : (a == b)^true & a -> b {
    use triv;
    use eq_to_right;

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

    let x2 = triv(x) : a == b;
    let r = eq_to_right(x2, y) : b;
    return r;
}

fn pow_elim_fst : p^(a & b) & a^true -> p^b {
    use pow_in_right_arg;
    use pow_transitivity;
    
    x : p^(a & b);
    y : a^true;
    
    fn f : a -> (a & b) == b {
        use refl;
        
        x : a;
        
        lam g1 : a & b => b {
            use snd;
            
            y : a & b;
            
            let r = snd(y) : b;
            return r;
        }
        lam g2 : b => a & b {
            use refl;
            
            y : b;
            
            let r = refl(x, y) : a & b;
            return r;
        }
        let r = refl(g1, g2) : (a & b) == b;
        return r;
    }
    let x2 = pow_transitivity(y, f) : ((a & b) == b)^true;
    let r = pow_in_right_arg(x, x2) : p^b;
    return r;
}

fn pow_elim_snd : p^(a & b) & b^true -> p^a {
    use pow_in_right_arg;
    use pow_transitivity;
    
    x : p^(a & b);
    y : b^true;
    
    fn f : b -> (a & b) == a {
        use refl;
        
        x : b;
        
        lam g1 : a & b => a {
            use fst;
            
            y : a & b;
            let r = fst(y) : a;
            return r;
        }
        lam g2 : a => a & b {
            use refl;
            
            y : a;
            let r = refl(y, x) : a & b;
            return r;
        }
        let r = refl(g1, g2) : (a & b) == a;
        return r;
    }
    let x2 = pow_transitivity(y, f) : ((a & b) == a)^true;
    let r = pow_in_right_arg(x, x2) : p^a;
    return r;
}

fn pow_elim : (a^b)^b -> a^b {
    use pow_transitivity;
    use pow_to_imply;
    use hooo_imply;
    use refl;

    x : (a^b)^b;

    let x2 = pow_to_imply() : (b => a)^(a^b);
    let x3 = pow_transitivity(x, x2) : (b => a)^b;
    let x4 = hooo_imply(x3) : b^b => a^b;
    let x5 = refl() : b^b;
    let r = x4(x5) : a^b;    
    return r;
}

fn hooo_imply_elim : (b => a)^b -> (b => a) {
    use hooo_imply;
    use refl;

    x : (b => a)^b;

    let x2 = hooo_imply(x) : b^b => a^b;
    let x3 = refl() : b^b;
    let r = x2(x3) : a^b;
    return r;
}

fn tauto_excm_to_or : (a | !a)^true -> a^true | (!a)^true {
    use hooo_or;

    x : (a | !a)^true;

    let r = hooo_or(x) : a^true | (!a)^true;
    return r;
}

fn tauto_reduce : a^true -> a^b {
    use pow_tr;
    use pow_transitivity;

    x : a^true;

    let x2 = pow_tr() : true^b;
    let r = pow_transitivity(x2, x) : a^b;
    return r;
}

fn tauto_excm_to_or_pow : excm(a)^true -> a^b | (!a)^b {
    x : excm(a)^true;

    use tauto_excm_to_or;
    let x2 = tauto_excm_to_or(x) : a^true | (!a)^true;
    lam f : a^true => a^b | (!a)^b {
        use left;
        use tauto_reduce;

        y : a^true;

        let y2 = tauto_reduce(y) : a^b;
        let r = left(y2) : a^b | (!a)^b;
        return r;
    }
    lam g : (!a)^true => a^b | (!a)^b {
        use right;
        use tauto_reduce;

        y : (!a)^true;

        let y2 = tauto_reduce(y) : (!a)^b;
        let r = right(y2) : a^b | (!a)^b;
        return r;
    }
    let r = match x2 (f, g) : a^b | (!a)^b;
    return r;
}

fn hooo_rev_not_excm : !(a^b) & excm(a)^true -> (!a)^b {
    use refl;
    use tauto_excm_to_or_pow;

    x : !(a^b);
    y : excm(a)^true;

    let x2 = tauto_excm_to_or_pow(y) : a^b | (!a)^b;
    lam f : a^b => (!a)^b {
        z : a^b;

        let z2 = x(z) : false;
        let r = match z2 : (!a)^b;
        return r;
    }
    let g = refl() : (!a)^b => (!a)^b;
    let r = match x2 (f, g) : (!a)^b;
    return r;
}

fn tauto_to_tauto_eq_true : a^true  ->  (a == true)^true {
    use pow_tr;
    use pow_eq_to_tauto_eq;

    x : a^true;

    let x2 = pow_tr() : true^a;
    let r = pow_eq_to_tauto_eq(x2, x) : (a == true)^true;
    return r;
}

fn tauto_eq_true_to_tauto : (a == true)^true  ->  a^true {
    use snd;
    use tauto_eq_to_pow_eq;

    x : (a == true)^true;

    let x2 = tauto_eq_to_pow_eq(x) : a =^= true;
    let r = snd(x2) : a^true;
    return r;
}

fn tauto_eq_symmetry : (a == b)^true  ->  (b == a)^true {
    use and_symmetry;
    use pow_eq_to_tauto_eq;
    use tauto_eq_to_pow_eq;

    x : (a == b)^true;

    let x2 = tauto_eq_to_pow_eq(x) : a =^= b;
    let x3 = and_symmetry(x2) : b =^= a;
    let r = pow_eq_to_tauto_eq(x3) : (b == a)^true;
    return r;
}