use cong;
use prop;

sym prop_eq;

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

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

fn eq_def : true -> prop_eq'(a, b) == (a == b) {
    use eq_cong;
    use eq_sym_def;
    use eq_ty;
    use cong_fun_bin_eq;
    use cong_fun_eq;
    use cong_in_arg;

    x : true;

    let y2 = eq_cong(x) : cong'(prop_eq');
    let y3 = eq_sym_def(x) : prop_eq' == sym(a, sym(b, a' == b'));
    let y4 = cong_in_arg(y2, y3) : cong'(sym(a, sym(b, a' == b')));
    let y5 = eq_ty(x) : (prop_eq' : prop' => prop' => prop');
    let y6 = cong_fun_bin_eq(y2, y4, y5, y3) :
        prop_eq'(a, b) == sym(a, sym(b, a' == b'))(a, b);
    let r = y6() : prop_eq'(a, b) == (a == b);
    return r;
}

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

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

    x : true;

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

fn eq_symmetry : a == b -> b == a {
    use fst;
    use snd;

    x : a == b;
    let y = fst(x) : a => b;
    let z = snd(x) : b => a;

    use refl;
    let r = refl(z, y) : b == a;
    return r;
}

fn eq_transitivity : (a == b) & (b == c)  -> (a == c) {
    use fst;
    use snd;

    x : a == b;
    y : b == c;
    let x1 = fst(x) : a => b;
    let x2 = snd(x) : b => a;
    let x3 = fst(y) : b => c;
    let x4 = snd(y) : c => b;

    use imply_transitivity;
    let x5 = imply_transitivity(x1, x3) : a => c;
    let x6 = imply_transitivity(x4, x2) : c => a;

    use refl;
    let x7 = refl(x5, x6) : a == c;
    return x7;
}

fn eq_transitivity_sym : (a == b) & (c == b)  ->  (a == c) {
    use eq_symmetry;
    use eq_transitivity;

    x : a == b;
    y : c == b;
    
    let y2 = eq_symmetry(y) : b == c;
    let r = eq_transitivity(x, y2) : a == c;
    return r;
}

fn eq_transitivity_rev_sym : (a == b) & (a == c) -> (b == c) {
    use eq_symmetry;
    use eq_transitivity;

    x : a == b;
    y : a == c;

    let x2 = eq_symmetry(x) : b == a;
    let r = eq_transitivity(x2, y) : b == c;
    return r;
}

fn eq_associativity :
    excm(a) & excm(b) & excm(c) -> ((a == b) == c) == (a == (b == c))
{
    use eq_from_and;
    use eq_rev_modus_tollens_excm;
    use eq_to_left;
    use eq_to_right;
    use imply_lift;
    use refl;

    x : excm(a);
    y : excm(b);
    z : excm(c);

    lam f : a => ((a == b) == c) == (a == (b == c)) {
        x2 : a;

        let to_a = imply_lift(x2) : (b == c) => a;
        lam f : b => ((a == b) == c) == (a == (b == c)) {
            y2 : b;

            let eq_a_b = eq_from_and(x2, y2) : a == b;
            let z6 = imply_lift(eq_a_b) : c => (a == b);
            lam f : c => ((a == b) == c) == (a == (b == c)) {
                z2 : c;

                let z4 = eq_from_and(y2, z2) : b == c;
                let z5 = imply_lift(z4) : a => (b == c);
                let z7 = refl(z5, to_a) : a == (b == c);
                let f = imply_lift(z7) : ((a == b) == c) => (a == (b == c));
                
                let z5 = imply_lift(z2) : (a == b) => c;
                let z7 = refl(z5, z6) : (a == b) == c;
                let g = imply_lift(z7) : (a == (b == c)) => ((a == b) == c);
                let r = refl(f, g) : ((a == b) == c) == (a == (b == c));
                return r;
            }
            lam g : !c => ((a == b) == c) == (a == (b == c)) {
                z2 : !c;

                lam f : ((a == b) == c) => (a == (b == c)) {
                    z3 : (a == b) == c;

                    let z4 = eq_to_right(z3, eq_a_b) : c;
                    let z5 = z2(z4) : false;    
                    let r = match z5 : a == (b == c);
                    return r;
                }
                lam g : (a == (b == c)) => ((a == b) == c) {
                    z3 : a == (b == c);

                    let z4 = eq_to_right(z3, x2) : b == c;
                    let z5 = eq_to_right(z4, y2) : c;
                    let z6 = z2(z5) : false;
                    let r = match z6 : (a == b) == c;
                    return r;
                }
                let r = refl(f, g) : ((a == b) == c) == (a == (b == c));
                return r;
            }
            let r = match z (f, g) : ((a == b) == c) == (a == (b == c));
            return r;
        }
        lam g : !b => ((a == b) == c) == (a == (b == c)) {
            y2 : !b;

            lam f : c => ((a == b) == c) == (a == (b == c)) {
                z2 : c;

                lam f : ((a == b) == c) => (a == (b == c)) {
                    z3 : (a == b) == c;
                    let eq_a_b = eq_to_left(z3, z2) : a == b;
                    let z4 = eq_to_right(eq_a_b, x2) : b;
                    let fa = y2(z4) : false;
                    let r = match fa : a == (b == c);
                    return r;
                }
                lam g : (a == (b == c)) => ((a == b) == c) {
                    z3 : a == (b == c);

                    let z4 = eq_to_right(z3, x2) : b == c;
                    let z5 = eq_to_left(z4, z2) : b;
                    let fa = y2(z5) : false;
                    let r = match fa : (a == b) == c;
                    return r;
                }
                let r = refl(f, g) : ((a == b) == c) == (a == (b == c));
                return r;
            }
            lam g : !c => ((a == b) == c) == (a == (b == c)) {
                z2 : !c;

                let z4 = eq_from_and(y2, z2) : !b == !c;
                let z5 = eq_rev_modus_tollens_excm(z4, y, z) : b == c;
                let f = imply_lift(z5) : a => (b == c);
                let g = imply_lift(x2) : (b == c) => a;
                let f = refl(f, g) : a == (b == c);
                let f = imply_lift(f) : ((a == b) == c) => (a == (b == c));
  
                lam g : (a == (b == c)) => ((a == b) == c) {
                    z3 : a == (b == c);

                    lam f : (a == b) => c {
                        z4 : a == b;

                        let z5 = eq_to_right(z4, x2) : b;
                        let z6 = y2(z5) : false;
                        let r = match z6 : c;
                        return r;
                    }
                    lam g : c => (a == b) {
                        z4 : c;
                        let z5 = z2(z4) : false;
                        let r = match z5 : a == b;
                        return r;
                    }
                    let r = refl(f, g) : (a == b) == c;
                    return r;
                }
                let r = refl(f, g) : ((a == b) == c) == (a == (b == c));
                return r;
            }
            let r = match z (f, g) : ((a == b) == c) == (a == (b == c));
            return r;
        }
        let r = match y (f, g) : ((a == b) == c) == (a == (b == c));
        return r;
    }
    lam g : !a => ((a == b) == c) == (a == (b == c)) {
       x2 : !a; 

       lam f : b => ((a == b) == c) == (a == (b == c)) {
            y2 : b;

            lam f : c => ((a == b) == c) == (a == (b == c)) {
                z2 : c;

                lam f : ((a == b) == c) => (a == (b == c)) {
                    z3 : (a == b) == c;

                    let eq_a_b = eq_to_left(z3, z2) : a == b;
                    let z5 = eq_to_left(eq_a_b, y2) : a;
                    let z6 = x2(z5) : false;
                    let r = match z6 : a == (b == c);
                    return r;
                }
                lam g : (a == (b == c)) => ((a == b) == c) {
                    z3 : a == (b == c);

                    let z4 = eq_from_and(y2, z2) : b == c;
                    let z5 = eq_to_left(z3, z4) : a;
                    let z6 = x2(z5) : false;
                    let r = match z6 : (a == b) == c;
                    return r;
                }
                let r = refl(f, g) : ((a == b) == c) == (a == (b == c));
                return r;
            }
            lam g : !c => ((a == b) == c) == (a == (b == c)) {
                z2 : !c;

                lam f : ((a == b) == c) => (a == (b == c)) {
                    z3 : (a == b) == c;

                    lam f : a => (b == c) {
                        z4 : a;

                        let z5 = x2(z4) : false;
                        let r = match z5 : b == c;
                        return r;
                    }
                    lam g : (b == c) => a {
                        z4 : b == c;

                        let z5 = eq_to_right(z4, y2) : c;
                        let z6 = z2(z5) : false;
                        let r = match z6 : a;
                        return r;
                    }
                    let r = refl(f, g) : a == (b == c);
                    return r;
                }
                lam g : (a == (b == c)) => ((a == b) == c) {
                    z3 : a == (b == c);

                    lam f : (a == b) => c {
                        z4 : a == b;

                        let z5 = eq_to_left(z4, y2) : a;
                        let z6 = x2(z5) : false;
                        let r = match z6 : c;
                        return r;
                    }
                    lam g : c => (a == b) {
                        z4 : c;

                        let z5 = z2(z4) : false;
                        let r = match z5 : a == b;
                        return r;
                    }
                    let r = refl(f, g) : (a == b) == c;
                    return r;
                }
                let r = refl(f, g) : ((a == b) == c) == (a == (b == c));
                return r;
            }
            let r = match z (f, g) : ((a == b) == c) == (a == (b == c));
            return r;
        }
        lam g : !b => ((a == b) == c) == (a == (b == c)) {
            y2 : !b;

            lam f : c => ((a == b) == c) == (a == (b == c)) {
                z2 : c;

                lam f : ((a == b) == c) => (a == (b == c)) {
                    z3 : (a == b) == c;

                    lam f : a => (b == c) {
                        z4 : a;

                        let z5 = x2(z4) : false;
                        let r = match z5 : b == c;
                        return r;
                    }
                    lam g : (b == c) => a {
                        z4 : b == c;

                        let z5 = eq_to_left(z4, z2) : b;
                        let z6 = y2(z5) : false;
                        let r = match z6 : a;
                        return r;
                    }
                    let r = refl(f, g) : a == (b == c);
                    return r;
                }
                lam g : (a == (b == c)) => ((a == b) == c) {
                    z3 : a == (b == c);

                    let f = imply_lift(z2) : (a == b) => c;
                    let z4 = refl(x2, y2) : !a & !b;
                    let z5 = eq_from_and(z4) : !a == !b;
                    let z6 = eq_rev_modus_tollens_excm(z5, x, y) : a == b;
                    let g = imply_lift(z6) : c => (a == b);
                    let r = refl(f, g) : (a == b) == c;
                    return r;
                }
                let r = refl(f, g) : ((a == b) == c) == (a == (b == c));
                return r;
            }
            lam g : !c => ((a == b) == c) == (a == (b == c)) {
                z2 : !c;

                lam f : ((a == b) == c) => (a == (b == c)) {
                    z3 : (a == b) == c;

                    let z4 = eq_from_and(x2, y2) : !a == !b;
                    let z5 = eq_rev_modus_tollens_excm(z4, x, y) : a == b;
                    let z6 = eq_to_right(z3, z5) : c;
                    let z7 = z2(z6) : false;
                    let r = match z7 : a == (b == c);
                    return r;
                }
                lam g : (a == (b == c)) => ((a == b) == c) {
                    z4 : a == (b == c);

                    let z5 = eq_from_and(y2, z2) : !b == !c;
                    let z6 = eq_rev_modus_tollens_excm(z5, y, z) : b == c;
                    let z7 = eq_to_left(z4, z6) : a;
                    let z8 = x2(z7) : false;
                    let r = match z8 : (a == b) == c;
                    return r;
                }
                let r = refl(f, g) : ((a == b) == c) == (a == (b == c));
                return r;
            }
            let r = match z (f, g) : ((a == b) == c) == (a == (b == c));
            return r;
        }
        let r = match y (f, g) : ((a == b) == c) == (a == (b == c));
        return r;
    }
    let r = match x (f, g) : ((a == b) == c) == (a == (b == c));
    return r;
}

fn eq_modus_tollens : (a == b)  ->  (!a == !b) {
    use fst;
    use modus_tollens;
    use refl;
    use snd;

    x : a == b;
 
    let x2 = fst(x) : a => b;
    let x3 = snd(x) : b => a; 
    let x4 = modus_tollens(x2) : !b => !a;
    let x5 = modus_tollens(x3) : !a => !b;
    let r = refl(x5, x4) : !a == !b;
    return r;
}

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

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

    let x2 = fst(x) : !a => !b;
    let x3 = snd(x) : !b => !a;
    let x4 = rev_modus_tollens_excm(x2, y, z) : b => a;
    let x5 = rev_modus_tollens_excm(x3, z, y) : a => b;
    let r = refl(x5, x4) : a == b;
    return r;
}

fn eq_to_left : (a == b) & b -> a {
    use snd;

    x : a == b;
    y : b;

    let x2 = snd(x) : b => a;
    let r = x2(y) : a;
    return r;
}

fn eq_to_right : (a == b) & a -> b {
    use fst;

    x : a == b;
    y : a;

    let x2 = fst(x) : a => b;
    let r = x2(y) : b;
    return r;
}

fn eq_from_and : a & b  ->  a == b {
    use imply_lift;
    use refl;

    x : a;
    y : b;

    let x2 = imply_lift(y) : a => b;
    let x3 = imply_lift(x) : b => a;
    let r = refl(x2, x3) : a == b;
    return r;
}

fn eq_eq_left : a == b -> (a == c) == (b == c) {
    use refl;

    x : a == b;

    lam f : (a == c) => (b == c) {
        use eq_transitivity_rev_sym;
    
        y : a == c;

        let r = eq_transitivity_rev_sym(x, y) : b == c;
        return r;
    }
    lam g : (b == c) => (a == c) {
        use eq_transitivity;

        y : b == c;

        let r = eq_transitivity(x, y) : a == c;
        return r;
    }
    let r = refl(f, g) : (a == c) == (b == c);
    return r;
}

fn eq_eq_right : a == b -> (c == a) == (c == b) {
    use refl;

    x : a == b;

    lam f : (c == a) => (c == b) {
        use eq_transitivity;

        y : c == a;

        let r = eq_transitivity(y, x) : c == b;
        return r;
    }
    lam g : (c == b) => (c == a) {
        use eq_transitivity_sym;

        y : c == b;

        let r = eq_transitivity_sym(y, x) : c == a;
        return r;
    }
    let r = refl(f, g) : (c == a) == (c == b);
    return r;
}

fn eq_tr : x -> x == true {
    use refl;

    x : x;

    lam f : x => true {
        let r = () : true;
        return r;
    }
    lam g : true => x {
        let r = x() : x;
        return r;
    }
    let r = refl(f, g) : x == true;
    return r;
}