Thm* e:(B B).
Thm* ( b:B. e(b) = b)
Thm* 
Thm* ( A:Type, f:(A A B). ( a:A. (Diag f wrt x. e(x)) = f(a))) | [diagonalization_wrt_eq] |
Thm* R:(B B Prop), e:(B B).
Thm* ( b:B. R(e(b),b))
Thm* 
Thm* ( A:Type, f:(A A B). ( a:A. R((Diag f wrt x. e(x))(a),f(a,a)))) | [diagonalization] |
Thm* A,B:Type, P:(A B Prop).
Thm* ( x:A. !y:B. P(x,y))  ( !f:(A B). x:A. P(x,f(x))) | [unique_indep_fun_description] |
Thm* ( x:A. !y:B. P(x,y))  ( f:(A B). x:A. P(x,f(x))) | [indep_fun_description] |
Thm* ( x:A. y:B. Q(x,y))  ( f:(A B). x:A. Q(x,f(x))) | [ax_choice_version2] |
Thm* B:(A Type), P:(x:A B(x) Prop).
Thm* ( x:A. !y:B(x). P(x,y))  ( ! {f:(x:A B(x))| x:A. P(x,f(x)) }) | [unique_fun_description2] |
Thm* B:(A Type), P:(x:A B(x) Prop).
Thm* ( x:A. !y:B(x). P(x,y))  ( !f:(x:A B(x)). x:A. P(x,f(x))) | [unique_fun_description] |
Thm* ( x:A. !y:B(x). P(x,y))  ( f:(x:A B(x)). x:A. P(x,f(x))) | [fun_description] |
Thm* ( x:A. y:B(x). Q(x,y))  ( f:(x:A B(x)). x:A. Q(x,f(x))) | [dep_ax_choice_version2] |
Thm* P:(A Type). ( x:A. Dec(P(x)))  ( ! {p:(A  )| x:A. p(x)  P(x) }) | [dec_pred_imp_bool_decider_exists] |
Thm* P:(A Prop). ( !u:A. P(u))  ( y,z:A. P(y)  P(z)  y = z) | [exists_unique_elim] |
Thm* R:(A A Prop).
Thm* (EquivRel x,y:A. R(x,y))
Thm* 
Thm* ( x:A. R(x,x) & ( y:A. R(x,y)  R(y,x) & ( z:A. R(y,z)  R(x,z)))) | [equivrel_characterization] |
Thm* ( x:A. B(x)  B'(x))  ({x:A| B(x) } =ext {x:A| B'(x) }) | [subset_sq_exteq] |
Thm* ( x:A. B(x)  B'(x))  {x:A| B(x) } {x:A| B'(x) } | [set_inc_wrt_imp_sq] |
Thm* x:A. B(x)  x {x:A| B(x) } | [squash_to_subset] |
Thm* ( x:A. B(x)  B'(x))  ({x:A| B(x) } =ext {x:A| B'(x) }) | [subset_exteq] |
Thm* ( x:A. B(x)  B'(x))  {x:A| B(x) } {x:A| B'(x) } | [set_inc_wrt_imp] |
Thm* Dec(P)  Dec( P) | [dec_imp_dec_sq] |
Thm* ( A)  ( ! (A B)) | [unique_fn_over_empty] |
Thm* ( ! A)  ( x:A. y:A. x = y) | [inhabited_uniquely_elim] |
Thm* ( x:T. Q(x))  ( x:T. Q(x)) | [not_over_exists_imp] |
Thm* Q:Prop(given P). Dec(P)  (P  Dec(Q))  Dec(P & Q) | [decidable__cand] |
Thm* Q:Prop(given P). P  Q Prop | [guarded_prop_to_prop] |
Thm* P Q  P  Q | [disjunct_elim] |
Thm* ( P:Prop.  P  P)  ( P:Prop. P P) | [negnegelim_vs_bivalence] |
Def x is the u:A. P(u) == P(x) & ( u:A. P(u)  u = x) | [is_the] |
Def x:A st P(x). Q(x) == x:A. P(x)  Q(x) | [allst] |