name: "std";
version: "0.2.0";
description: "Standard library for Hooo";
functions {
  1 : 1';
  2 : 2';
  E : E';
  Excm : Excm';
  K : K';
  Lob : Lob';
  N : N';
  N2 : N2';
  NecToPos : NecToPos';
  PosToNec : PosToNec';
  T : T';
  absurd : false -> a;
  add : add';
  all_pow_absurd : all(a -> b) -> c;
  and : and';
  and_associativity : true -> (((a & b) & c) == (a & (b & c)));
  and_cong : true -> cong'(prop_and');
  and_def : true -> (prop_and'(a, b) == (a & b));
  and_eq_left : (a == b) -> ((a & c) == (b & c));
  and_eq_right : (a == b) -> ((c & a) == (c & b));
  and_map : a -> (b => (a & b));
  and_ntauto_npara_to_theory : (!(a^true) & !(false^a)) -> theory'(a);
  and_sym_def : true -> (prop_and' == sym(a, sym(b, a' & b')));
  and_symmetry : (a & b) -> (b & a);
  and_to_eq : (a & b) -> (a == b);
  and_transitivity : ((a & b) & (b & c)) -> (a & c);
  and_ty : true -> (prop_and' : prop' => (prop' => prop'));
  ava_ava : ((a, b(c)) & (b(c) : d)) -> (d(a) => b(c));
  ava_collide : ((b, q1(a1)) & ((b, q2(a2)) & ((q1(a1) : p) & (q2(a2) : p)))) -> !(sd(q1, q2));
  ava_lower_univ : (!~p & ((b, a) & (a : p))) -> (p(b) == a);
  ava_univ : (!~b & ((a, b) & (b : c))) -> (c(a) == b);
  bool : bool';
  bool_absurd : (fa' == tr') -> false;
  bool_and_cong : true -> cong'(and');
  bool_and_fa : true -> (and'(fa') == fa1');
  bool_and_fa_fa : true -> (and'(fa', fa') == fa');
  bool_and_fa_tr : true -> (and'(fa', tr') == fa');
  bool_and_in_left_arg : ((and'(a, b) == c) & (a == d)) -> (and'(d, b) == c);
  bool_and_in_right_arg : ((and'(a, b) == c) & (b == d)) -> (and'(a, d) == c);
  bool_and_same : (a : bool') -> (and'(a, a) == a);
  bool_and_symmetry : ((a : bool') & (b : bool')) -> (and'(a, b) == and'(b, a));
  bool_and_tr : true -> (and'(tr') == idb');
  bool_and_tr_fa : true -> (and'(tr', fa') == fa');
  bool_and_tr_tr : true -> (and'(tr', tr') == tr');
  bool_and_ty : true -> (and' : bool' => (bool' => bool'));
  bool_def : (a : bool') -> ((a == fa') | (a == tr'));
  bool_eq_idb_self : (a : bool') -> (idb'(a) == a);
  bool_eq_not_not_self : (a : bool') -> (not'(not'(a)) == a);
  bool_fa1 : (a : bool') -> (fa1'(a) == fa');
  bool_fa1_cong : true -> cong'(fa1');
  bool_fa1_in_arg : ((fa1'(a) == b) & (a == c)) -> (fa1'(c) == b);
  bool_fa1_ty : true -> (fa1' : bool' => bool');
  bool_fa_ty : true -> (fa' : bool');
  bool_fun_eq : ((f : bool' => c) & ((g : bool' => c) & (f == g))) -> (f(a) == g(a));
  bool_idb_cong : true -> cong'(idb');
  bool_idb_fa : true -> (idb'(fa') == fa');
  bool_idb_in_arg : ((idb'(a) == b) & (a == c)) -> (idb'(c) == b);
  bool_idb_in_arg_sym : ((idb'(a) == b) & (c == a)) -> (idb'(c) == b);
  bool_idb_tr : true -> (idb'(tr') == tr');
  bool_idb_ty : true -> (idb' : bool' => bool');
  bool_not_cong : true -> cong'(not');
  bool_not_fa : true -> (not'(fa') == tr');
  bool_not_in_arg : ((not'(a) == b) & (a == c)) -> (not'(c) == b);
  bool_not_in_arg_sym : ((not'(a) == b) & (c == a)) -> (not'(c) == b);
  bool_not_tr : true -> (not'(tr') == fa');
  bool_not_ty : true -> (not' : bool' => bool');
  bool_or_cong : true -> cong'(or');
  bool_or_fa : true -> (or'(fa') == idb');
  bool_or_tr : true -> (or'(tr') == tr1');
  bool_or_ty : true -> (or' : bool' => (bool' => bool'));
  bool_tr1 : (a : bool') -> (tr1'(a) == tr');
  bool_tr1_cong : true -> cong'(tr1');
  bool_tr1_in_arg : ((tr1'(a) == b) & (a == c)) -> (tr1'(c) == b);
  bool_tr1_ty : true -> (tr1' : bool' => bool');
  bool_tr_ty : true -> (tr' : bool');
  bool_ty : true -> (bool' : type'(z'));
  c_imply_to_excm : (!a | a) -> excm(a);
  c_imply_transitivity : ((!a | b) & (!b | c)) -> (!a | c);
  comp_cong : (cong'(f) & cong'(g)) -> cong'(f . g);
  comp_def : true -> ((f . g)(a) == f(g(a)));
  comp_tup_def : (cong'(f) & (cong'(g) & cong'(h))) -> ((h . (f, g))(a) == h(f(a), g(a)));
  comp_tup_sym_def : true -> ((h . (f, g)) == sym(a, h(f(a'), g(a'))));
  comp_tup_sym_eq : true -> (sym(a, (h . (f, g))(a')) == (h . (f, g)));
  comp_ty : ((f : a -> b) & (g : b -> c)) -> ((f . g) : a -> c);
  cong : cong';
  cong_app : (cong'(f) & (f : t1 => (t2 => t3))) -> cong'(f(a));
  cong_app_eq : (cong'(f) & (a == b)) -> (f(a) == f(b));
  cong_app_in_arg : (cong'(f) & ((f(a) == b) & (a == c))) -> (f(c) == b);
  cong_bin : (cong'(f) & (cong'(g) & cong'(h))) -> cong'(sym(a, h(f(a'), g(a'))));
  cong_bin_and : (cong'(f) & cong'(g)) -> cong'(sym(a, f(a') & g(a')));
  cong_bin_eq : (cong'(f) & cong'(g)) -> cong'(sym(a, f(a') == g(a')));
  cong_bin_eq_fst : cong'(f) -> cong'(sym(a, f(a') == a'));
  cong_bin_fst : (cong'(f) & cong'(h)) -> cong'(sym(a, h(f(a'), a')));
  cong_bin_imply : (cong'(f) & cong'(g)) -> cong'(sym(a, f(a') => g(a')));
  cong_bin_or : (cong'(f) & cong'(g)) -> cong'(sym(a, f(a') | g(a')));
  cong_cong : true -> cong'(cong');
  cong_def : true -> (cong'(f) == sym(f, all((a == b) -> (f'(a) == f'(b))))(f));
  cong_eq : (f == g) -> (cong'(f) == cong'(g));
  cong_eq_both : (cong'(f) & ((f : t1 => (t2 => t3)) & ((a == b) & (c == d)))) -> (f(a, c) == f(b, d));
  cong_eq_left : (cong'(f) & ((f : t1 => (t2 => t3)) & (a == b))) -> (f(a, c) == f(b, c));
  cong_eq_right : (cong'(f) & ((f : t1 => (t2 => t3)) & (a == b))) -> (f(c, a) == f(c, b));
  cong_eq_to_tauto_eq : sym(f, all((a == b) -> (f'(a) == f'(b))))(f) -> sym(f, all((a == b)^true -> (f'(a) == f'(b))))(f);
  cong_from : sym(f, all((a == b) -> (f'(a) == f'(b))))(f) -> cong'(f);
  cong_fun_bin_eq : (cong'(f) & (cong'(g) & ((f : t1 => (t2 => t3)) & (f == g)))) -> (f(a, b) == g(a, b));
  cong_fun_eq : (cong'(f) & (cong'(g) & (f == g))) -> (f(a) == g(a));
  cong_in_arg : (cong'(f) & (f == g)) -> cong'(g);
  cong_in_both_args : (cong'(f) & ((f : t1 => (t2 => t3)) & (f(a, b) & ((a == c) & (b == d))))) -> f(c, d);
  cong_in_left_arg : (cong'(f) & ((f : t1 => (t2 => t3)) & (f(a, b) & (a == c)))) -> f(c, b);
  cong_in_right_arg : (cong'(f) & ((f : t1 => (t2 => t3)) & (f(a, b) & (b == c)))) -> f(a, c);
  cong_sym : true -> cong'(sym(f, all((a == b) -> (f'(a) == f'(b)))));
  cong_sym_def : true -> (cong' == sym(f, all((a == b) -> (f'(a) == f'(b)))));
  cong_sym_id : true -> cong'(sym(a, a'));
  cong_to : cong'(f) -> sym(f, all((a == b) -> (f'(a) == f'(b))))(f);
  cong_to_tauto_cong : cong'(f) -> tauto_cong'(f);
  curry : ((a & b) => c) -> (a => (b => c));
  e_from : all(excm(!a)) -> E';
  e_to : E' -> all(excm(!a));
  eq_associativity : (excm(a) & (excm(b) & excm(c))) -> (((a == b) == c) == (a == (b == c)));
  eq_cong : true -> cong'(prop_eq');
  eq_def : true -> (prop_eq'(a, b) == (a == b));
  eq_eq_left : (a == b) -> ((a == c) == (b == c));
  eq_eq_right : (a == b) -> ((c == a) == (c == b));
  eq_from_and : (a & b) -> (a == b);
  eq_modus_tollens : (a == b) -> (!a == !b);
  eq_q_qu : true -> ((a ~~ a) == ~a);
  eq_qu_q : true -> (~a == (a ~~ a));
  eq_refl : true -> (a == a);
  eq_rev_modus_tollens_excm : ((!a == !b) & (excm(a) & excm(b))) -> (a == b);
  eq_sym_def : true -> (prop_eq' == sym(a, sym(b, a' == b')));
  eq_symmetry : (a == b) -> (b == a);
  eq_to_left : ((a == b) & b) -> a;
  eq_to_right : ((a == b) & a) -> b;
  eq_tr : x -> (x == true);
  eq_transitivity : ((a == b) & (b == c)) -> (a == c);
  eq_transitivity_rev_sym : ((a == b) & (a == c)) -> (b == c);
  eq_transitivity_sym : ((a == b) & (c == b)) -> (a == c);
  eq_ty : true -> (prop_eq' : prop' => (prop' => prop'));
  ex : ex';
  excm_from : all(excm(a)) -> Excm';
  excm_n_to_e_imply : (excm(!a) & excm(!b)) -> ((!a | b) | ((!b | a) | (!!a & !!b)));
  excm_n_to_e_triple : excm(!a) -> (a | excm(!a));
  excm_or_imply_left : excm(a) -> ((a => b) | (b => a));
  excm_or_imply_right : excm(b) -> ((a => b) | (b => a));
  excm_to : Excm' -> all(excm(a));
  excm_to_c_imply : excm(a) -> (!a | a);
  exists_from : !((!b)^a) -> ex'(a, b);
  exists_from_imply : !(a => !b) -> ex'(a, b);
  exists_to : ex'(a, b) -> !((!b)^a);
  exists_true_to_npara : ex'(true, a) -> !(false^a);
  fa : fa';
  fa1 : fa1';
  fst : (a & b) -> a;
  hooo_and : (a & b)^c -> (a^c & b^c);
  hooo_comp : (c^b & b^a) -> c^a;
  hooo_dual_or : c^(a | b) -> (c^a & c^b);
  hooo_dual_rev_and : (c^a | c^b) -> c^(a & b);
  hooo_dual_rev_or : (c^a & c^b) -> c^(a | b);
  hooo_imply : (a => b)^c -> (a^c => b^c);
  hooo_imply_elim : (b => a)^b -> (b => a);
  hooo_or : (a | b)^c -> (a^c | b^c);
  hooo_rev_and : (a^c & b^c) -> (a & b)^c;
  hooo_rev_not_excm : (!(a^b) & excm(a)^true) -> (!a)^b;
  hooo_rev_or : (a^c | b^c) -> (a | b)^c;
  id : id';
  id_cong : true -> cong'(id');
  id_def : ((n : nat') & ((t : type'(n)) & (a : t))) -> (id'(t, a) == a);
  id_def_nat : (a : nat') -> (id'(nat', a) == a);
  id_def_type0 : ((t : type'(z')) & (a : t)) -> (id'(t, a) == a);
  idb : idb';
  imply_cong : true -> cong'(prop_imply');
  imply_def : true -> (prop_imply'(a, b) == (a => b));
  imply_eq_left : (a == b) -> ((a => c) == (b => c));
  imply_eq_right : (a == b) -> ((c => a) == (c => b));
  imply_excm_left_to_or : ((a => b) & excm(a)) -> (!a | b);
  imply_excm_right_to_or : ((a => b) & excm(b)) -> (!a | b);
  imply_from_or : (!a | b) -> (a => b);
  imply_in_left_arg : ((a => b) & (a == c)) -> (c => b);
  imply_in_right_arg : ((a => b) & (b == c)) -> (a => c);
  imply_lift : a -> (b => a);
  imply_refl : true -> (a => a);
  imply_sym_def : true -> (prop_imply' == sym(a, sym(b, a' => b')));
  imply_transitivity : ((a => b) & (b => c)) -> (a => c);
  imply_ty : true -> (prop_imply' : prop' => (prop' => prop'));
  inv : inv';
  inv_cong : true -> cong'(inv');
  inv_eq : (f == g) -> (inv'(f) == inv'(g));
  inv_involve_eq : true -> (inv'(inv'(f)) == f);
  inv_ty : (f : a -> b) -> (inv'(f) : b -> a);
  inv_val_qu : (~inv'(f) & (f(a) == b)) -> (inv'(f, b) == a);
  left : a -> (a | b);
  liar_not : (a =^= !a) -> false;
  liar_para : (a =^= false^a) -> false;
  lob_absurd : all((p^true => p)^true => p^true) -> false;
  lob_triv : (p^true => p)^true;
  modal_k_from : all(□(a => b) => (□a => □b)) -> K';
  modal_k_to : K' -> all(□(a => b) => (□a => □b));
  modal_lob_from : all(□(□a => a) => □a) -> Lob';
  modal_lob_to : Lob' -> all(□(□a => a) => □a);
  modal_n2_from : all(□a == (a^true)) -> N2';
  modal_n2_to : N2' -> all(□a == (a^true));
  modal_n2_to_k : N2' -> K';
  modal_n2_to_n : N2' -> N';
  modal_n2_to_nlob : N2' -> !Lob';
  modal_n2_to_t_2 : N2' -> T';
  modal_n_from : all(a^true => □a) -> N';
  modal_n_to : N' -> all(a^true => □a);
  modal_n_to_nlob : (N' & false^(□false)) -> !Lob';
  modal_nec_eq : (a == b) -> (□a == □b);
  modal_nec_in_arg : (□a & (a == b)) -> □b;
  modal_nec_to_pos_from : all(□a == !◇!a) -> NecToPos';
  modal_nec_to_pos_to : NecToPos' -> all(□a == !◇!a);
  modal_pos_eq : (a == b) -> (◇a == ◇b);
  modal_pos_in_arg : (◇a & (a == b)) -> ◇b;
  modal_pos_to_nec_from : all(◇a == !□!a) -> PosToNec';
  modal_pos_to_nec_to : PosToNec' -> all(◇a == !□!a);
  modal_t_from : all(□a => a) -> T;
  modal_t_to : T' -> all(□a => a);
  modal_tauto_excm_to_imply_nec_to_pos_pos_to_nec : all(excm(a)^true) -> (NecToPos' => PosToNec');
  modal_tauto_excm_to_imply_pos_to_nec_nec_to_pos : all(excm(a)^true) -> (PosToNec' => NecToPos');
  modal_tauto_n2_to_para_nec_false : N2'^true -> false^(□false);
  modal_tauto_t_to_para_nec_false : T'^true -> false^(□false);
  modus_ponens : (a & (a => b)) -> b;
  modus_tollens : (a => b) -> (!b => !a);
  nat : nat';
  nat_add_check_all_ty : ((a : nat') & (b : nat')) -> (add'(a, b) : nat');
  nat_add_cong : true -> cong'(add');
  nat_add_eq_both : ((a == c) & (b == d)) -> (add'(a, b) == add'(c, d));
  nat_add_eq_left : (a == b) -> (add'(a, c) == add'(b, c));
  nat_add_eq_right : (a == b) -> (add'(c, a) == add'(c, b));
  nat_add_from_zero_left : ((a : nat') & (add'(a, z') == z')) -> (a == z');
  nat_add_from_zero_right : ((a : nat') & (add'(z', a) == z')) -> (a == z');
  nat_add_succ : ((a : nat') & (b : nat')) -> (add'(a, s'(b)) == s'(add'(a, b)));
  nat_add_succ_right : ((a : nat') & (b : nat')) -> (add'(s'(a), b) == s'(add'(a, b)));
  nat_add_succ_symmetry : ((a : nat') & (b : nat')) -> (add'(s'(a), b) == add'(a, s'(b)));
  nat_add_sym_symmetry_cong : true -> cong'(sym(a, (b : nat') => (add'(a', b) == add'(b, a'))));
  nat_add_symmetry : ((a : nat') & (b : nat')) -> (add'(a, b) == add'(b, a));
  nat_add_ty : true -> (add' : nat' => (nat' => nat'));
  nat_add_zero : (a : nat') -> (add'(a, z') == a);
  nat_add_zero_left : (a : nat') -> (add'(z', a) == a);
  nat_add_zero_left_cong : true -> cong'(sym(a, add'(z', a') == a'));
  nat_add_zero_symmetry : (a : nat') -> (add'(a, z') == add'(z', a));
  nat_cover : (b^(a == z') & b^((prev'(a) : nat') & (a == s'(prev'(a))))) -> b^(a : nat');
  nat_def : (a : nat') -> ((a == z') | ((prev'(a) : nat') & (a == s'(prev'(a)))));
  nat_eq_prev_lower : (prev'(a) == prev'(b)) -> (a == b);
  nat_eq_prev_to_eq : ((prev'(a) == prev'(b)) & ((a == s'(prev'(a))) & (b == s'(prev'(b))))) -> (a == b);
  nat_eq_succ_lower : (s'(a) == s'(b)) -> (a == b);
  nat_ex_ind : (ex'(z' : nat', a) & ex'(s'(n) : nat', a)^(n : nat')) -> a;
  nat_ind : (cong'(p)^true & (p(z')^true & sym(p, all((p'(a) => p'(s'(a)))^(a : nat')))(p))) -> p(b)^(b : nat');
  nat_neq_zero_one : true -> !(z' == s'(z'));
  nat_one_eq : true -> (1' == s'(z'));
  nat_one_from : s'(z') -> 1';
  nat_one_plus_one_equals_two : true -> (add'(1', 1') == 2');
  nat_one_to : 1' -> s'(z');
  nat_one_ty : true -> (1' : nat');
  nat_para_eq_prev : (a == prev'(a)) -> false;
  nat_para_eq_succ : ((a : nat') & (a == s'(a))) -> false;
  nat_para_eq_zero_pos : (z' == s'(a)) -> false;
  nat_para_eq_zero_prev_succ : (z' == prev'(s'(z'))) -> false;
  nat_para_eq_zero_succ_prev : (z' == s'(prev'(z'))) -> false;
  nat_prev_cong : true -> cong'(prev');
  nat_prev_eq : (a == b) -> (prev'(a) == prev'(b));
  nat_prev_ind : (cong'(p) & (prev'(a) : nat')) -> (sym(p, all(p'(prev'(b)) => p'(s'(prev'(b)))))(p) => p(a));
  nat_prev_symmetry : (a : nat') -> (s'(prev'(a)) == prev'(s'(a)));
  nat_prev_to_eq_succ_prev : (prev'(a) : nat') -> (a == s'(prev'(a)));
  nat_prev_to_nzero : (prev'(a) : nat') -> !(a == z');
  nat_prev_ty : ((a : nat') & (a == s'(prev'(a)))) -> (prev'(a) : nat');
  nat_succ_cong : true -> cong'(s');
  nat_succ_eq : (a == b) -> (s'(a) == s'(b));
  nat_succ_ty : (a : nat') -> (s'(a) : nat');
  nat_sym_add_case1_cong : true -> cong'(sym(b, (a : nat') => (add'(s'(a), b') == s'(add'(a, b')))));
  nat_sz_ty : true -> (s'(z') : nat');
  nat_two_eq : true -> (2' == s'(s'(z')));
  nat_two_from : s'(s'(z')) -> 2';
  nat_two_to : 2' -> s'(s'(z'));
  nat_two_ty : true -> (2' : nat');
  nat_ty : true -> (nat' : type'(z'));
  nat_zero_ty : true -> (z' : nat');
  nec : nec';
  nec_cong : true -> cong'(nec');
  nec_def : true -> (nec'(a) == □a);
  neq_to_sesh : !(a == b) -> !(a ~~ b);
  nleft : !(a | b) -> !a;
  nnexcm : true -> !!excm(a);
  nor_tauto_para_to_theory : !(a^true | false^a) -> theory'(a);
  norm1 : norm1';
  norm2 : norm2';
  not : not';
  not_double : a -> !!a;
  not_excm_to_eq_nn : excm(a) -> (a == !!a);
  not_rev_double_excm : (!!a & excm(a)) -> a;
  not_rev_triple : !!!a -> !a;
  not_to_not_tauto : !a -> !(a^true);
  npara_to_exists_true : !(false^a) -> ex'(true, a);
  nqu_to_nsd : !~a -> !(sd(a, a));
  nqu_to_qu_inv : !~a -> ~!a;
  nqu_to_sesh : !~a -> !(a ~~ a);
  nright : !(a | b) -> !b;
  or : or';
  or_associativity : true -> (((a | b) | c) == (a | (b | c)));
  or_cong : true -> cong'(prop_or');
  or_def : true -> (prop_or'(a, b) == (a | b));
  or_eq_left : (a == b) -> ((a | c) == (b | c));
  or_eq_right : (a == b) -> ((c | a) == (c | b));
  or_sym_def : true -> (prop_or' == sym(a, sym(b, a' | b')));
  or_symmetry : (a | b) -> (b | a);
  or_ty : true -> (prop_or' : prop' => (prop' => prop'));
  par : par';
  par_app : (cong'(f) & cong'(g)) -> (par'(f, g, (a, b)) == (f(a), g(b)));
  par_cong : (cong'(f) & cong'(g)) -> cong'(par'(f, g));
  par_def : true -> (par'(f, g) == (f . tup_fst', g . tup_snd'));
  para_liar : ((false^a)^(a^true) & ((a^true)^(false^a) & excm(a)^true)) -> false;
  para_lob : ((!(false^true))^true => false^true) -> false;
  para_nexcm : !excm(a) -> false;
  para_to_not : false^a -> !a;
  para_to_tauto_not : false^a -> (!a)^true;
  para_to_uniform : false^a -> uniform'(a);
  path_eq_sym_norm1_norm1 : true -> (sym_norm1'(f, g) == norm1'(f, g, g));
  path_norm1_def : true -> (norm1'(f, g1, g2) == (g2 . f . inv'(g1)));
  path_norm1_to_sym_norm1 : norm1'(f, g, g) -> sym_norm1'(f, g);
  path_norm2_def : true -> (norm2'(f, g1, g2, g3) == (g3 . f . (inv'(g1), inv'(g2))));
  path_sym_norm1_def : true -> (sym_norm1'(f, g) == (g . f . inv'(g)));
  path_sym_norm1_to_norm1 : sym_norm1'(f, g) -> norm1'(f, g, g);
  path_sym_norm2_def : true -> (sym_norm2'(f, g) == (g . f . (inv'(g), inv'(g))));
  pos : pos';
  pos_cong : true -> cong'(pos');
  pos_def : true -> (pos'(a) == ◇a);
  pow_and_lift : (a^b & c^d) -> (a^b & c^d)^e;
  pow_elim : (a^b)^b -> a^b;
  pow_elim_fst : (p^(a & b) & a^true) -> p^b;
  pow_elim_snd : (p^(a & b) & b^true) -> p^a;
  pow_eq_to_tauto_eq : (a =^= b) -> (a == b)^true;
  pow_in_left_arg : (a^b & (a == c)^true) -> c^b;
  pow_in_right_arg : (a^b & (b == c)^true) -> a^c;
  pow_lift : a^b -> (a^b)^c;
  pow_modus_tollens : (a -> b) -> (!b -> !a);
  pow_or_lift : (a^b | c^d) -> (a^b | c^d)^e;
  pow_to_imply : b^a -> (a => b);
  pow_to_imply_lift : b^a -> (a => b)^c;
  pow_to_pow_tauto : a^b -> a^(b^true);
  pow_to_tauto_imply : a^b -> (b => a)^true;
  pow_tr : a -> true;
  pow_transitivity : (b^a & c^b) -> c^a;
  prev : prev';
  prop : prop';
  prop_and : prop_and';
  prop_eq : prop_eq';
  prop_imply : prop_imply';
  prop_or : prop_or';
  ps_core : ((a ~~ b) & ((a : c) & (b : d))) -> (c ~~ d);
  ps_nqu_mem : (!~b & (a : b)) -> !~a;
  ps_sesh_mem : (!(b ~~ b) & (a : b)) -> !(a ~~ a);
  q : q';
  q_def : true -> (q'(a, b) == (a ~~ b));
  q_from : ((a == b) & (~a & ~b)) -> (a ~~ b);
  q_left : (a ~~ b) -> (a ~~ a);
  q_lift : ((sd(a, b)) & (a == b)) -> (a ~~ b);
  q_right : (a ~~ b) -> (b ~~ b);
  q_symmetry : (a ~~ b) -> (b ~~ a);
  q_tauto_cong : true -> tauto_cong'(q');
  q_to : (a ~~ b) -> ((a == b) & (~a & ~b));
  q_to_eq : (a ~~ b) -> (a == b);
  q_to_qu : (a ~~ a) -> ~a;
  q_transitivity : ((a ~~ b) & (b ~~ c)) -> (a ~~ c);
  qu : qu';
  qu_def : true -> (qu'(a) == ~a);
  qu_eq_inv : true -> (~!a == !~a);
  qu_in_arg : (~a & (a == b)^true) -> ~b;
  qu_inv_to_nqu : ~!a -> !~a;
  qu_qu_true_tauto_excm_to_tauto : (~a & (~true & excm(a)^true)) -> a^true;
  qu_tauto_cong : true -> tauto_cong'(qu');
  qu_to_q : ~a -> (a ~~ a);
  qu_true_tauto_excm_to_eq_tauto_qu : (~true & excm(a)^true) -> ((a^true) == ~a);
  refl : a -> a;
  rev_modus_tollens_excm : ((!a => !b) & (excm(a) & excm(b))) -> (b => a);
  rev_modus_tollens_nn : (!!a => !!b) -> (!b => !a);
  right : b -> (a | b);
  s : s';
  sd : sd';
  sd_conv_eq_from : (sd'(a, b) == sd'(c, d)) -> ((sd(a, b)) == (sd(c, d)));
  sd_conv_eq_to : ((sd(a, b)) == (sd(c, d))) -> (sd'(a, b) == sd'(c, d));
  sd_conv_from : sd'(a, b) -> (sd(a, b));
  sd_conv_to : (sd(a, b)) -> sd'(a, b);
  sd_def : true -> (sd'(a, b) == (sd(a, b)));
  sd_eq_both : ((a == b)^true & (c == d)^true) -> ((sd(a, c)) == (sd(b, d)));
  sd_eq_left : (a == b)^true -> ((sd(a, c)) == (sd(b, c)));
  sd_eq_right : (a == b)^true -> ((sd(c, a)) == (sd(c, b)));
  sd_in_left_arg : ((sd(a, b)) & (a == c)^true) -> (sd(c, b));
  sd_in_right_arg : ((sd(a, b)) & (b == c)^true) -> (sd(a, c));
  sd_symmetry : (sd(a, b)) -> (sd(b, a));
  sd_tauto_cong : true -> tauto_cong'(sd');
  sd_to_q : (sd(a, a)) -> (a ~~ a);
  sd_to_qu : (sd(a, a)) -> ~a;
  sd_ty : true -> (sd' : prop' => (prop' => prop'));
  sesh_left : !(a ~~ a) -> !(a ~~ b);
  sesh_right : !(b ~~ b) -> !(a ~~ b);
  sesh_to_nsd : !(a ~~ a) -> !(sd(a, a));
  snd : (a & b) -> b;
  sym_absurd : (a & sym(a, all(a' -> b))(a)) -> false;
  sym_all_conv : sym(a, all(a'))(a) -> sym(b, all(b'))(a);
  sym_all_pow_absurd : all(a -> b) -> false;
  sym_cong_eq : (cong'(sym(c, a)) & (a == b)^(sym c)) -> (sym(c, a)(x) == sym(c, b)(x));
  sym_eq : (a == b)^(sym c) -> (sym(c, a) == sym(c, b));
  sym_eq_refl : (sym a) -> (a' == a');
  sym_from : sym(a, a')(a) -> a;
  sym_from_all : sym(a, all(a'))(a) -> a;
  sym_fun_eq : true -> (sym(a, f(a')) == f);
  sym_norm1 : sym_norm1';
  sym_norm2 : sym_norm2';
  sym_pow_lift : a^b -> sym(a, all(a'))(a)^sym(b, all(b'))(b);
  sym_pow_to_pow_tauto : sym(f, a^b)(f) -> sym(f, a^(b^true))(f);
  sym_to_all : a -> sym(a, all(a'))(a);
  sym_transitivity : (sym(a, b) & (b => c)^(sym a)) -> sym(a, c);
  sym_transport : (sym(a, b) & (b == c)^(sym a)) -> sym(a, c);
  sym_unwrap : sym(a, b)(a) -> b;
  tauto_cong : tauto_cong';
  tauto_cong_app : (tauto_cong'(f) & (f : t1 => (t2 => t3))) -> tauto_cong'(f(a));
  tauto_cong_app_eq : (tauto_cong'(f) & (a == b)^true) -> (f(a) == f(b));
  tauto_cong_app_in_arg : (tauto_cong'(f) & ((f(a) == b) & (a == c)^true)) -> (f(c) == b);
  tauto_cong_eq_both : (tauto_cong'(f)^true & ((f : t1 => (t2 => t3)) & ((a == b)^true & (c == d)^true))) -> (f(a, c) == f(b, d));
  tauto_cong_eq_left : (tauto_cong'(f)^true & ((f : t1 => (t2 => t3)) & (a == b)^true)) -> (f(a, c) == f(b, c));
  tauto_cong_eq_right : (tauto_cong'(f) & ((f : t1 => (t2 => t3)) & (a == b)^true)) -> (f(c, a) == f(c, b));
  tauto_cong_from : sym(f, all((a == b)^true -> (f'(a) == f'(b))))(f) -> tauto_cong'(f);
  tauto_cong_fun_eq : (tauto_cong'(f) & (tauto_cong'(g) & (f == g)^true)) -> (f(a) == g(a));
  tauto_cong_in_arg : (tauto_cong'(f) & (f == g)^true) -> tauto_cong'(g);
  tauto_cong_in_both_args : (tauto_cong'(f)^true & ((f : t1 => (t2 => t3)) & (f(a, b) & ((a == c)^true & (b == d)^true)))) -> f(c, d);
  tauto_cong_in_left_arg : (tauto_cong'(f)^true & ((f : t1 => (t2 => t3)) & (f(a, b) & (a == c)^true))) -> f(c, b);
  tauto_cong_in_right_arg : (tauto_cong'(f) & ((f : t1 => (t2 => t3)) & (f(a, b) & (b == c)^true))) -> f(a, c);
  tauto_cong_sym : true -> tauto_cong'(sym(f, all((a == b)^true -> (f'(a) == f'(b)))));
  tauto_cong_to : tauto_cong'(f) -> sym(f, all((a == b)^true -> (f'(a) == f'(b))))(f);
  tauto_eq_refl : true -> (a == a);
  tauto_eq_symmetry : (a == b)^true -> (b == a)^true;
  tauto_eq_tauto_not_para : true -> (((!a)^true) == (false^a));
  tauto_eq_to_left : ((a == b)^true & b) -> a;
  tauto_eq_to_pow_eq : (a == b)^true -> (a =^= b);
  tauto_eq_to_right : ((a == b)^true & a) -> b;
  tauto_eq_true_to_tauto : (a == true)^true -> a^true;
  tauto_excm_to_or : excm(a)^true -> (a^true | (!a)^true);
  tauto_excm_to_or_pow : excm(a)^true -> (a^b | (!a)^b);
  tauto_excm_to_uniform : excm(a)^true -> uniform'(a);
  tauto_hooo_and : (a & b)^c -> (a^c & b^c)^true;
  tauto_hooo_imply : (a => b)^c -> (a^c => b^c)^true;
  tauto_hooo_or : (a | b)^c -> (a^c | b^c)^true;
  tauto_hooo_rev_and : (a^c & b^c)^true -> (a & b)^c;
  tauto_imply_refl : true -> (a => a);
  tauto_imply_to_pow : (a => b)^true -> b^a;
  tauto_nnexcm : true -> !!excm(a);
  tauto_not_to_para : (!a)^true -> false^a;
  tauto_q_to_tauto_eq : (a ~~ b)^true -> (a == b)^true;
  tauto_qu_true_to_qu : (a^true & ~true) -> ~a;
  tauto_reduce : a^true -> a^b;
  tauto_to_tauto_eq_true : a^true -> (a == true)^true;
  tauto_to_uniform : a^true -> uniform'(a);
  tauto_uniform_eq : true -> (uniform'(a) == (a^true | false^a));
  theory : theory';
  theory_to : theory'(a) -> !(a^true | false^a);
  theory_to_npara : theory'(a) -> !(false^a);
  theory_to_ntauto : theory'(a) -> !(a^true);
  theory_to_uniform : theory'(a) -> !uniform'(a);
  tr : tr';
  tr1 : tr1';
  triv : a^true -> a;
  tup_app : true -> ((f, g)(a) == (f(a), g(a)));
  tup_comp_both_cong : (cong'(f) & cong'(g)) -> cong'((f . tup_fst', g . tup_snd'));
  tup_comp_fst : cong'(f) -> ((f . tup_fst')((a, b)) == f(a));
  tup_comp_fst_cong : cong'(f) -> cong'(f . tup_fst');
  tup_comp_snd : cong'(f) -> ((f . tup_snd')((a, b)) == f(b));
  tup_comp_snd_cong : cong'(f) -> cong'(f . tup_snd');
  tup_cong : (cong'(f) & cong'(g)) -> cong'((f, g));
  tup_eq_both : ((a == b) & (c == d)) -> ((a, c) == (b, d));
  tup_eq_left : (a == b) -> ((a, c) == (b, c));
  tup_eq_right : (a == b) -> ((c, a) == (c, b));
  tup_fst : tup_fst';
  tup_fst_cong : true -> cong'(tup_fst');
  tup_fst_def : true -> (tup_fst'((a, b)) == a);
  tup_fst_ty : true -> (tup_fst : (a, b) -> a);
  tup_inv_def : true -> (inv'((f, g)) == (inv'(f), inv'(g)));
  tup_snd : tup_snd';
  tup_snd_cong : true -> cong'(tup_snd');
  tup_snd_def : true -> (tup_snd'((a, b)) == b);
  tup_snd_ty : true -> (tup_snd : (a, b) -> b);
  tup_ty : ((a : c) & (b : d)) -> ((a, b) : (c, d));
  ty_app : ((f : a => b) & (a2 : a)) -> (f(a2) : b);
  ty_app2 : ((f : a => (b => c)) & ((a2 : a) & (b2 : b))) -> (f(a2, b2) : c);
  ty_eq_left : (a == b) -> ((a : c) == (b : c));
  ty_eq_right : (a == b) -> ((c : a) == (c : b));
  ty_fun : ((a : at) & (b : bt)) -> ((a => b) : at => bt);
  ty_fun_ty : true -> (type'(a) => (type'(b) : type'(z')));
  ty_in_left_arg : ((a : b) & (a == c)) -> (c : b);
  ty_in_right_arg : ((a : b) & (b == c)) -> (a : c);
  ty_judgement : (b : type'(n)) -> ((a : b) : type'(n));
  ty_lift : unsafe' -> ((a : x) -> (a : a : x));
  ty_sd_to_neq : ((sd(a, b)) & ((a : type'(z')) & (b : type'(z')))) -> !(a == b);
  ty_transitivity : ((a : b) & (b : c)) -> (a : c);
  ty_tup_ty : ((a : x) & (b : y)) -> ((a, b) : (x, y));
  ty_tup_type : true -> ((type'(n), type'(m)) : type'(z'));
  ty_uniq : (!(a == b) & ((c : a) == (c : b))) -> false;
  type : type';
  uncurry : (a => (b => c)) -> ((a & b) => c);
  uniform : uniform';
  uniform_from : (a^true | false^a) -> uniform'(a);
  uniform_to : uniform'(a) -> (a^true | false^a);
  uniform_to_tauto_excm : uniform'(a) -> excm(a)^true;
  uniform_to_theory : !uniform'(a) -> theory'(a);
  unify : ((a | b) & ((a => c) & (b => c))) -> c;
  unsafe : unsafe';
  z : z';
}
dependencies {
}