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_version3] |
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* ( x:T. Dec(E(x)))  ( f:(T  ). x:T. f(x)  E(x)) | [dec_pred_iff_some_boolfun] |
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* ( Set:Type, :(Set Set Prop).
Thm* ( P:(Set Prop). p:Set. x:Set. (x p)  P(x)) | [RussellsParadox_Frege2] |
Thm* ( A:Type, Q:(A A Prop). P:(A Prop). p:A. x:A. Q(x,p)  P(x)) | [RussellsParadox_Frege] |
Thm* (P  P) | [no_prop_iff_its_neg] |
Thm* A:Type. (A Discrete) Prop | [is_discrete_wf] |
Thm* {x:A| if b P(x) else Q(x) fi }
Thm* =ext
Thm* if b {x:A| P(x) } else {x:A| Q(x) } fi | [ifthenelse_distr_subtype] |
Thm* {x:A| P(x) } =ext {x:A| P(x) } | [subset_squash_exteq] |
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:{x:A| B(x) }. B(x) | [subset_to_squash] |
Thm* ( x:A. B(x)  B'(x))  ({x:A| B(x) } =ext {x:A| B'(x) }) | [subset_exteq] |
Thm* {x:{x:A| P(x) }| Q(x) } =ext {x:A| P(x) & Q(x) } | [exteq_subset_vs_and] |
Thm* P XOR Q  (Q  P) & Dec(P) | [xor_vs_neg_n_dec] |
Thm* P,Q:Prop. (P XOR Q) Prop | [xor_wf] |
Thm* ( x:A. B(x)  B'(x))  {x:A| B(x) } {x:A| B'(x) } | [set_inc_wrt_imp] |
Thm*  P  P | [sq_sq_iff_sq] |
Thm* Dec(P)  Dec( P) | [dec_imp_dec_sq] |
Thm* ( P)  P | [sq_not_iff_sq] |
Thm*  P  P | [not_sq_iff_sq] |
Thm* F:(Prop Prop). ( P:Prop. F(P))  ( A:Type. F( A)) | [inhab_rep_eqv] |
Thm* A:Type. P = ( A) Prop | [inhab_rep_axiom] |
Thm* B:(A Type), P:(A Prop).
Thm* (i:{i:A| P(i) } B(i)) =ext {v:(i:A B(i))| P(v/x,y. x) } | [exteq_sigma_st_dom] |
Thm* ( x:T. Q(x))  ( x:T. Q(x)) | [not_over_exists_imp] |
Thm* Dec(P)  ( b: . b  P) | [decbl_iff_some_bool] |
Thm* B:Prop(given A). (A & B) Prop | [cand_is_prop] |
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* Q Q  Q | [or_fused] |
Thm* P Q  P  Q | [disjunct_elim] |
Thm* ( P:Prop.  P  P)  ( P:Prop. P P) | [negnegelim_vs_bivalence] |