core_2 Theory

Summary of Definitions

Typed Definitions

so_apply1 *

so_apply2 *

so_apply3 *

so_apply4 *

so_apply5 *

so_apply6 *

so_apply7 *

infix_ap *

so_lambda1 *

so_lambda2 *

label *

guard *1

error *

prop *

cand *

parameter *

ycomb *

icomb *1

kcomb *1

scomb *1

pi1 *2

pi2 *4

spread3 *

spread4 *

spread5 *

spread6 *

spread7 *

it *1

decidable *1

stable *1

sq_stable *1

subtype *1

suptype *

let *3

type_inj *

xmiddle *1

choicef *9

singleton *1

unique_set *1

uni_sat *1

Main Theorems

pair_eta_rw *3

unit_triviality *2

decidable__or *6

decidable__and *6

decidable__implies *7

decidable__false *1

decidable__not *1

decidable__iff *2

decidable__int_equal *2

decidable__lt *2

decidable__le *4

decidable__atom_equal *13

iff_preserves_decidability *5

decidable_functionality *7

stable__not *4

stable__function_equal *8

stable__from_decidable *2

sq_stable__and *7

sq_stable__implies *4

sq_stable__iff *4

sq_stable__all *4

sq_stable__equal *2

sq_stable__squash *3

sq_stable__from_stable *6

sq_stable__not *4

sq_stable_from_decidable *4

sq_stable_iff_stable *9

squash_elim *3

dneg_elim *2

dneg_elim_a *3

iff_symmetry *1

and_assoc *1

and_comm *1

or_assoc *1

or_comm *1

not_over_or *6

not_over_or_a *1

not_over_and_b *2

not_over_and *6

and_false_l *1

and_false_r *1

and_true_l *1

and_true_r *1

or_false_l *1

or_false_r *1

or_true_l *1

or_true_r *1

exists_over_and_r *3

equal_symmetry *1

iff_transitivity *2

implies_transitivity *1

and_functionality_wrt_iff *1

and_functionality_wrt_implies *1

implies_functionality_wrt_iff *1

implies_functionality_wrt_implies *1

iff_functionality_wrt_iff *1

all_functionality_wrt_iff *1

all_functionality_wrt_implies *2

exists_functionality_wrt_iff *5

exists_functionality_wrt_implies *3

not_functionality_wrt_iff *1

not_functionality_wrt_implies *4

or_functionality_wrt_iff *5

or_functionality_wrt_implies *3

squash_functionality_wrt_implies *2

implies_antisymmetry *1

gen_hyp_tp *88

choicef_lemma *1

fun_thru_spread *4

spread_to_pi12 *4

uni_sat_imp_in_uni_set *4

sq_stable__uni_sat *1