use cong;
use z;
use type;

sym bool;
sym tr;
sym fa;
sym fa1;
sym not;
sym idb;
sym tr1;
sym and;
sym or;

fn bool_ty : true -> (bool' : type'(z')) {
    axiom bool_ty : true -> (bool' : type'(z'));
    x : true;
    let r = bool_ty(x) : (bool' : type'(z'));
    return r;
}

fn bool_tr_ty : true -> (tr' : bool') {
    axiom bool_tr_ty : true -> (tr' : bool');
    x : true;
    let r = bool_tr_ty(x) : (tr' : bool');
    return r;
}

fn bool_fa_ty : true -> (fa' : bool') {
    axiom bool_fa_ty : true -> (fa' : bool');
    x : true;
    let r = bool_fa_ty(x) : (fa' : bool');
    return r;
}

fn bool_def : (a : bool') -> (a == fa') | (a == tr') {
    axiom bool_def : (a : bool') -> (a == fa') | (a == tr');
    x : (a : bool');
    let r = bool_def(x) : (a == fa') | (a == tr');
    return r;
}

fn bool_absurd : fa' == tr' -> false {
    axiom bool_absurd : fa' == tr' -> false;
    x : fa' == tr';
    let r = bool_absurd(x) : false;
    return r;
}

fn bool_fun_eq : (f : bool' => c) & (g : bool' => c) & (f == g) -> f(a) == g(a) {
    axiom bool_fun_eq : (f : bool' => c) & (g : bool' => c) & (f == g) -> f(a) == g(a);
    x : (f : bool' => c) & (g : bool' => c) & (f == g);
    let r = bool_fun_eq(x) : f(a) == g(a);
    return r;
}

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

fn bool_fa1_ty : true -> (fa1' : bool' => bool') {
    axiom bool_fa1_ty : true -> (fa1' : bool' => bool');
    x : true;
    let r = bool_fa1_ty(x) : (fa1' : bool' => bool');
    return r;
}

fn bool_fa1 : (a : bool') -> fa1'(a) == fa' {
    axiom bool_fa1 : (a : bool') -> fa1'(a) == fa';
    x : (a : bool');
    let r = bool_fa1(x) : fa1'(a) == fa';
    return r;
}

fn bool_fa1_in_arg : (fa1'(a) == b) & (a == c) -> fa1'(c) == b {
    use cong_app_in_arg;
    use bool_fa1_cong;
    use triv;
    x : fa1'(a) == b;
    y : a == c;
    let fa1_cong = triv(bool_fa1_cong) : cong'(fa1');
    let r = cong_app_in_arg(fa1_cong, x, y) : fa1'(c) == b;
    return r;
}

fn bool_not_ty : true -> (not' : bool' => bool') {
    axiom bool_not_ty : true -> (not' : bool' => bool');
    x : true;
    let r = bool_not_ty(x) : (not' : bool' => bool');
    return r;
}

fn bool_not_tr : true -> not'(tr') == fa' {
    axiom bool_not_tr : true -> not'(tr') == fa';
    x : true;
    let r = bool_not_tr(x) : not'(tr') == fa';
    return r;
}

fn bool_not_fa : true -> not'(fa') == tr' {
    axiom bool_not_fa : true -> not'(fa') == tr';
    x : true;
    let r = bool_not_fa(x) : not'(fa') == tr';
    return r;
}

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

fn bool_not_in_arg : (not'(a) == b) & (a == c) -> (not'(c) == b) {
    use cong_app_in_arg;
    use bool_not_cong;
    use triv;

    x : not'(a) == b;
    y : a == c;
    let not_cong = triv(bool_not_cong) : cong'(not');
    let r = cong_app_in_arg(not_cong, x, y) : not'(c) == b;
    return r;
}

fn bool_not_in_arg_sym : (not'(a) == b) & (c == a) -> (not'(c) == b) {
    use bool_not_in_arg;
    use eq_symmetry;

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

fn bool_idb_ty : true -> (idb' : bool' => bool') {
    axiom bool_idb_ty : true -> (idb' : bool' => bool');
    x : true;
    let r = bool_idb_ty(x) : (idb' : bool' => bool');
    return r;
}

fn bool_idb_tr : true -> idb'(tr') == tr' {
    axiom bool_idb_tr : true -> idb'(tr') == tr';
    x : true;
    let r = bool_idb_tr(x) : idb'(tr') == tr';
    return r;
}

fn bool_idb_fa : true -> idb'(fa') == fa' {
    axiom bool_idb_fa : true -> idb'(fa') == fa';
    x : true;
    let r = bool_idb_fa(x) : idb'(fa') == fa';
    return r;
}

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

fn bool_idb_in_arg : (idb'(a) == b) & (a == c) -> (idb'(c) == b) {
    use cong_app_in_arg;
    use bool_idb_cong;
    use triv;

    x : idb'(a) == b;
    y : a == c;
    let idb_cong = triv(bool_idb_cong) : cong'(idb');
    let r = cong_app_in_arg(idb_cong, x, y) : idb'(c) == b;
    return r;
}

fn bool_idb_in_arg_sym : (idb'(a) == b) & (c == a) -> (idb'(c) == b) {
    use bool_idb_in_arg;
    use eq_symmetry;

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

fn bool_tr1_ty : true -> (tr1' : bool' => bool') {
    axiom bool_tr1_ty : true -> (tr1' : bool' => bool');
    x : true;
    let r = bool_tr1_ty(x) : (tr1' : bool' => bool');
    return r;
}

fn bool_tr1 : (a : bool') -> tr1'(a) == tr' {
    axiom bool_tr1 : (a : bool') -> tr1'(a) == tr';
    x : (a : bool');
    let r = bool_tr1(x) : tr1'(a) == tr';
    return r;
}

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

fn bool_tr1_in_arg : (tr1'(a) == b) & (a == c) -> tr1'(c) == b {
    use cong_app_in_arg;
    use bool_tr1_cong;
    use triv;

    x : tr1'(a) == b;
    y : a == c;
    let tr1_cong = triv(bool_tr1_cong) : cong'(tr1');
    let r = cong_app_in_arg(tr1_cong, x, y) : tr1'(c) == b;
    return r;
}

fn bool_eq_idb_self : (a : bool') -> idb'(a) == a {
    x : (a : bool');
    use bool_def;
    let x2 = bool_def(x) : (a == fa') | (a == tr');
    lam f : (a == fa') => idb'(a) == a {
        use bool_idb_in_arg_sym;
        use bool_idb_fa;
        use eq_transitivity_sym;
        use triv;

        y : a == fa';

        let y2 = triv(bool_idb_fa) : idb'(fa') == fa';
        let y3 = bool_idb_in_arg_sym(y2, y) : idb'(a) == fa';
        let r = eq_transitivity_sym(y3, y) : idb'(a) == a;
        return r;
    }
    lam g : (a == tr') => idb'(a) == a {
        use bool_idb_in_arg_sym;
        use bool_idb_tr;
        use eq_transitivity_sym;
        use triv;

        y : a == tr';

        let y2 = triv(bool_idb_tr) : idb'(tr') == tr';
        let y3 = bool_idb_in_arg_sym(y2, y) : idb'(a) == tr';
        let r = eq_transitivity_sym(y3, y) : idb'(a) == a;
        return r;
    }
    let r = match x2 (f, g) : idb'(a) == a;
    return r;
}

fn bool_eq_not_not_self : (a : bool') -> not'(not'(a)) == a {
    use bool_def;
    use bool_not_fa;
    use bool_not_tr;
    use triv;

    x : (a : bool');

    let eq_fa_tr = bool_def(x) : (a == fa') | (a == tr');
    let not_fa = triv(bool_not_fa) : (not'(fa') == tr');
    let not_tr = triv(bool_not_tr) : (not'(tr') == fa');

    lam f : (a == fa') => not'(not'(a)) == a {
        use bool_not_in_arg_sym;
        use eq_transitivity_sym;

        y : a == fa';

        let y2 = bool_not_in_arg_sym(not_fa, y) : not'(a) == tr';
        let y3 = bool_not_in_arg_sym(not_tr, y2) : not'(not'(a)) == fa';
        let r = eq_transitivity_sym(y3, y) : not'(not'(a)) == a;
        return r;
    }
    lam g : (a == tr') => not'(not'(a)) == a {
        use bool_not_in_arg_sym;
        use eq_transitivity_sym;

        y : a == tr';

        let y2 = bool_not_in_arg_sym(not_tr, y) : not'(a) == fa';
        let y3 = bool_not_in_arg_sym(not_fa, y2) : not'(not'(a)) == tr';
        let r = eq_transitivity_sym(y3, y) : not'(not'(a)) == a;
        return r;
    }
    let r = match eq_fa_tr (f, g) : not'(not'(a)) == a;
    return r;
}

fn bool_and_ty : true -> (and' : bool' => bool' => bool') {
    axiom bool_and_ty : true -> (and' : bool' => bool' => bool');
    x : true;
    let r = bool_and_ty(x) : (and' : bool' => bool' => bool');
    return r;
}

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

fn bool_and_fa : true -> and'(fa') == fa1' {
    axiom bool_and_fa : true -> and'(fa') == fa1';
    x : true;
    let r = bool_and_fa(x) : and'(fa') == fa1';
    return r;
}

fn bool_and_tr : true -> and'(tr') == idb' {
    axiom bool_and_tr : true -> and'(tr') == idb';
    x : true;
    let r = bool_and_tr(x) : and'(tr') == idb';
    return r;
}

fn bool_and_fa_fa : true -> and'(fa', fa') == fa' {
    use bool_and_fa;
    use bool_and_ty;
    use bool_fa_ty;
    use bool_fa1_ty;
    use bool_fun_eq;
    use bool_fa1;
    use eq_transitivity;
    use triv;
    use ty_app;

    x : true;

    let y2 = triv(bool_and_fa) : and'(fa') == fa1';
    let fa1_ty = triv(bool_fa1_ty) : (fa1' : bool' => bool');
    let fa_ty = triv(bool_fa_ty) : (fa' : bool');
    let and_ty = triv(bool_and_ty) : (and' : bool' => bool' => bool');
    let and_fa_ty = ty_app(and_ty, fa_ty) : (and'(fa') : bool' => bool');
    let y3 = bool_fun_eq(and_fa_ty, fa1_ty, y2) : and'(fa', fa') == fa1'(fa');
    let y4 = bool_fa1(fa_ty) : fa1'(fa') == fa';
    let r = eq_transitivity(y3, y4) : and'(fa', fa') == fa';
    return r;
}

fn bool_and_fa_tr : true -> and'(fa', tr') == fa' {
    use bool_and_fa;
    use bool_and_ty;
    use bool_fa_ty;
    use bool_fa1;
    use bool_fa1_ty;
    use bool_tr_ty;
    use bool_fun_eq;
    use bool_tr1_ty;
    use eq_transitivity;
    use triv;
    use ty_app;

    x : true;

    let fa_ty = triv(bool_fa_ty) : (fa' : bool');
    let tr_ty = triv(bool_tr_ty) : (tr' : bool');
    let fa1_ty = triv(bool_fa1_ty) : (fa1' : bool' => bool');
    let y2 = triv(bool_and_fa) : and'(fa') == fa1';
    let tr1_ty = triv(bool_tr1_ty) : (tr1' : bool' => bool');
    let and_ty = triv(bool_and_ty) : (and' : bool' => bool' => bool');
    let and_fa_ty = ty_app(and_ty, fa_ty) : (and'(fa') : bool' => bool');
    let y3 = bool_fun_eq(and_fa_ty, fa1_ty, y2) : and'(fa', tr') == fa1'(tr');
    let y4 = bool_fa1(tr_ty) : fa1'(tr') == fa';
    let r = eq_transitivity(y3, y4) : and'(fa', tr') == fa';
    return r;
}

fn bool_and_tr_fa : true -> and'(tr', fa') == fa' {
    use bool_and_tr;
    use bool_and_ty;
    use bool_fun_eq;
    use bool_idb_fa;
    use bool_idb_ty;
    use bool_tr_ty;
    use eq_transitivity;
    use triv;
    use ty_app;

    x : true;

    let and_ty = triv(bool_and_ty) : (and' : bool' => bool' => bool');
    let tr_ty = triv(bool_tr_ty) : (tr' : bool');
    let y6 = ty_app(and_ty, tr_ty) : (and'(tr') : bool' => bool');
    let y5 = triv(bool_idb_ty) : (idb' : bool' => bool');
    let y4 = triv(bool_and_tr) : and'(tr') == idb';
    let y3 = bool_fun_eq(y6, y5, y4) : and'(tr', fa') == idb'(fa');
    let y2 = triv(bool_idb_fa) : idb'(fa') == fa';
    let r = eq_transitivity(y3, y2) : and'(tr', fa') == fa';
    return r;
}

fn bool_and_tr_tr : true -> and'(tr', tr') == tr' {
    use bool_and_tr;
    use bool_and_ty;
    use bool_fun_eq;
    use bool_idb_tr;
    use bool_idb_ty;
    use bool_tr_ty;
    use eq_transitivity;
    use triv;
    use ty_app;

    x : true;

    let and_ty = triv(bool_and_ty) : (and' : bool' => bool' => bool');
    let tr_ty = triv(bool_tr_ty) : (tr' : bool');
    let y6 = ty_app(and_ty, tr_ty) : (and'(tr') : bool' => bool');
    let y5 = triv(bool_idb_ty) : (idb' : bool' => bool');
    let y4 = triv(bool_and_tr) : and'(tr') == idb';
    let y3 = bool_fun_eq(y6, y5, y4) : and'(tr', tr') == idb'(tr');
    let y2 = triv(bool_idb_tr) : idb'(tr') == tr';
    let r = eq_transitivity(y3, y2) : and'(tr', tr') == tr';
    return r;
}

fn bool_and_same : (a : bool') -> and'(a, a) == a {
    use bool_def;

    x : (a : bool');

    let x2 = bool_def(x) : (a == fa') | (a == tr');

    lam f : (a == fa') => (and'(a, a) == a) {
        use bool_and_cong;
        use bool_and_fa_fa;
        use bool_and_ty;
        use cong_app;
        use cong_app_eq;
        use bool_fa_ty;
        use cong_fun_eq;
        use eq_symmetry;
        use eq_transitivity;
        use triv;
        use ty_app;

        y : a == fa';

        let and_ty = triv(bool_and_ty) : (and' : bool' => bool' => bool');
        let and_cong = triv(bool_and_cong) : cong'(and');
        let and_a_cong = cong_app(and_cong, and_ty) : cong'(and'(a));
        let y7 = cong_app_eq(and_a_cong, y) : and'(a, a) == and'(a, fa');
        let and_fa_cong = cong_app(and_cong, and_ty) : cong'(and'(fa'));
        let y6 = cong_app_eq(and_cong, y) : and'(a) == and'(fa');
        let y5 = cong_fun_eq(and_a_cong, and_fa_cong, y6) : and'(a, fa') == and'(fa', fa');
        let y4 = eq_transitivity(y7, y5) : and'(a, a) == and'(fa', fa');
        let y3 = eq_symmetry(y) : fa' == a;
        let y2 = triv(bool_and_fa_fa) : and'(fa', fa') == fa';
        let y1 = eq_transitivity(y4, y2) : and'(a, a) == fa';
        let r = eq_transitivity(y1, y3) : and'(a, a) == a;
        return r;
    }
    lam g : (a == tr') => (and'(a, a) == a) {
        use bool_and_tr;
        use bool_and_ty;
        use bool_and_cong;
        use cong_app_eq;
        use bool_eq_idb_self;
        use bool_fun_eq;
        use bool_idb_cong;
        use eq_symmetry;
        use eq_transitivity;
        use triv;
        use cong_app;
        use cong_fun_eq;

        y : a == tr';

        let and_ty = triv(bool_and_ty) : (and' : bool' => bool' => bool');
        let and_cong = triv(bool_and_cong) : cong'(and');
        let y6 = triv(bool_and_tr) : and'(tr') == idb';
        let y5 = cong_app_eq(and_cong, y) : and'(a) == and'(tr');
        let and_a_cong = cong_app(and_cong, and_ty) : cong'(and'(a));
        let idb_cong = triv(bool_idb_cong) : cong'(idb');
        let y4 = eq_transitivity(y5, y6) : and'(a) == idb';
        let y3 = cong_fun_eq(and_a_cong, idb_cong, y4) : and'(a, a) == idb'(a);
        let y2 = bool_eq_idb_self(x) : idb'(a) == a;
        let r = eq_transitivity(y3, y2) : and'(a, a) == a;
        return r;
    }
    let r = match x2 (f, g) : and'(a, a) == a;
    return r;
}

fn bool_and_in_left_arg :
    (and'(a, b) == c) & (a == d) -> and'(d, b) == c
{
    use bool_and_cong;
    use bool_and_ty;
    use cong_app_eq;
    use cong_fun_eq;
    use eq_symmetry;
    use eq_transitivity;
    use triv;
    use cong_app;

    x : and'(a, b) == c;
    y : a == d;

    let and_ty = triv(bool_and_ty) : (and' : bool' => bool' => bool');
    let and_cong = triv(bool_and_cong) : cong'(and');
    let and_d_cong = cong_app(and_cong, and_ty) : cong'(and'(d));
    let and_a_cong = cong_app(and_cong, and_ty) : cong'(and'(a));
    let y2 = eq_symmetry(y) : d == a;
    let x3 = cong_app_eq(and_cong, y2) : and'(d) == and'(a);
    let x2 = cong_fun_eq(and_d_cong, and_a_cong, x3) : and'(d, b) == and'(a, b);
    let r = eq_transitivity(x2, x) : and'(d, b) == c;
    return r;
}

fn bool_and_in_right_arg :
    (and'(a, b) == c) & (b == d) -> and'(a, d) == c
{
    use bool_and_cong;
    use bool_and_ty;
    use cong_app;
    use cong_app_eq;
    use eq_symmetry;
    use eq_transitivity;
    use triv;

    x : and'(a, b) == c;
    y : b == d;

    let and_ty = triv(bool_and_ty) : (and' : bool' => bool' => bool');
    let y2 = eq_symmetry(y) : d == b;
    let and_cong = triv(bool_and_cong) : cong'(and');
    let x3 = cong_app(and_cong, and_ty) : cong'(and'(a));
    let x2 = cong_app_eq(x3, y2) : and'(a, d) == and'(a, b);
    let r = eq_transitivity(x2, x) : and'(a, d) == c;
    return r;
}

fn bool_and_symmetry : (a : bool') & (b : bool') -> and'(a, b) == and'(b, a) {
    use bool_def;

    x : (a : bool');
    y : (b : bool');

    let x2 = bool_def(x) : (a == fa') | (a == tr');
    let y2 = bool_def(y) : (b == fa') | (b == tr');
    lam f1 : (a == fa') => (b == fa') => and'(a, b) == and'(b, a) {
        x3 : a == fa';
        lam r : (b == fa') => and'(a, b) == and'(b, a) {
            use bool_and_fa_fa;
            use bool_and_in_left_arg;
            use bool_and_in_right_arg;
            use eq_symmetry;
            use eq_transitivity_sym;
            use triv;

            x4 : b == fa';

            let y3 = eq_symmetry(x3) : fa' == a;
            let y4 = eq_symmetry(x4) : fa' == b;
            let and_fa_fa = triv(bool_and_fa_fa) : and'(fa', fa') == fa';
            let x5 = bool_and_in_left_arg(and_fa_fa, y3) : and'(a, fa') == fa';
            let x6 = bool_and_in_right_arg(x5, y4) : and'(a, b) == fa';
            let x7 = bool_and_in_left_arg(and_fa_fa, y4) : and'(b, fa') == fa';
            let x8 = bool_and_in_right_arg(x7, y3) : and'(b, a) == fa';
            let r = eq_transitivity_sym(x6, x8) : and'(a, b) == and'(b, a);
            return r;
        }
        return r;
    }
    lam f2 : (a == tr') => (b == fa') => and'(a, b) == and'(b, a) {
        x3 : a == tr';
        lam r : (b == fa') => and'(a, b) == and'(b, a) {
            use bool_and_in_left_arg;
            use bool_and_in_right_arg;
            use bool_and_fa_tr;
            use bool_and_tr_fa;
            use eq_symmetry;
            use eq_transitivity_sym;
            use triv;

            x4 : b == fa';

            let y3 = eq_symmetry(x3) : tr' == a;
            let y4 = eq_symmetry(x4) : fa' == b;
            let and_tr_fa = triv(bool_and_tr_fa) : and'(tr', fa') == fa';
            let x5 = bool_and_in_left_arg(and_tr_fa, y3) : and'(a, fa') == fa';
            let x6 = bool_and_in_right_arg(x5, y4) : and'(a, b) == fa';
            let and_fa_tr = triv(bool_and_fa_tr) : and'(fa', tr') == fa';
            let x7 = bool_and_in_left_arg(and_fa_tr, y4) : and'(b, tr') == fa';
            let x8 = bool_and_in_right_arg(x7, y3) : and'(b, a) == fa';
            let r = eq_transitivity_sym(x6, x8) : and'(a, b) == and'(b, a);
            return r;
        }
        return r;
    }
    lam f3 : (a == fa') => (b == tr') => and'(a, b) == and'(b, a) {
        x3 : a == fa';
        lam r : (b == tr') => and'(a, b) == and'(b, a) {
            use bool_and_fa_tr;
            use bool_and_tr_fa;
            use bool_and_in_left_arg;
            use bool_and_in_right_arg;
            use eq_symmetry;
            use eq_transitivity_sym;
            use triv;

            x4 : b == tr';

            let y3 = eq_symmetry(x3) : fa' == a;
            let y4 = eq_symmetry(x4) : tr' == b;
            let and_fa_tr = triv(bool_and_fa_tr) : and'(fa', tr') == fa';
            let x5 = bool_and_in_left_arg(and_fa_tr, y3) : and'(a, tr') == fa';
            let x6 = bool_and_in_right_arg(x5, y4) : and'(a, b) == fa';
            let and_tr_fa = triv(bool_and_tr_fa) : and'(tr', fa') == fa';
            let x7 = bool_and_in_left_arg(and_tr_fa, y4) : and'(b, fa') == fa';
            let x8 = bool_and_in_right_arg(x7, y3) : and'(b, a) == fa';
            let r = eq_transitivity_sym(x6, x8) : and'(a, b) == and'(b, a);
            return r;
        }
        return r;
    }
    lam f4 : (a == tr') => (b == tr') => and'(a, b) == and'(b, a) {
        x3 : a == tr';
        lam r : (b == tr') => and'(a, b) == and'(b, a) {
            use bool_and_tr_tr;
            use bool_and_in_left_arg;
            use bool_and_in_right_arg;
            use eq_symmetry;
            use eq_transitivity_sym;
            use triv;

            x4 : b == tr';

            let y3 = eq_symmetry(x3) : tr' == a;
            let y4 = eq_symmetry(x4) : tr' == b;
            let and_tr_tr = triv(bool_and_tr_tr) : and'(tr', tr') == tr';
            let x5 = bool_and_in_left_arg(and_tr_tr, y3) : and'(a, tr') == tr';
            let x6 = bool_and_in_right_arg(x5, y4) : and'(a, b) == tr';
            let x7 = bool_and_in_left_arg(and_tr_tr, y4) : and'(b, tr') == tr';
            let x8 = bool_and_in_right_arg(x7, y3) : and'(b, a) == tr';
            let r = eq_transitivity_sym(x6, x8) : and'(a, b) == and'(b, a);
            return r;
        }
        return r;
    }
    let f5 = match x2 (f1, f2) : (b == fa') => and'(a, b) == and'(b, a);
    let f6 = match x2 (f3, f4) : (b == tr') => and'(a, b) == and'(b, a);
    let r = match y2 (f5, f6) : and'(a, b) == and'(b, a);
    return r;
}

fn bool_or_ty : true -> (or' : bool' => bool' => bool') {
    axiom bool_or_ty : true -> (or' : bool' => bool' => bool');
    x : true;
    let r = bool_or_ty(x) : (or' : bool' => bool' => bool');
    return r;
}

fn bool_or_fa : true -> or'(fa') == idb' {
    axiom bool_or_fa : true -> or'(fa') == idb';
    x : true;
    let r = bool_or_fa(x) : or'(fa') == idb';
    return r;
}

fn bool_or_tr : true -> or'(tr') == tr1' {
    axiom bool_or_tr : true -> or'(tr') == tr1';
    x : true;
    let r = bool_or_tr(x) : or'(tr') == tr1';
    return r;
}

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