COM | sqequal_com | Here are the essentials: ... |
COM | sq_type_com | There are other types in Nuprl that we can consider first order types. ... |
def | sq_type |
|
THM | int_sq |
|
THM | nat_sq |
|
THM | bool_sq |
|
THM | atom_sq |
|
THM | bool_sim_true |
|
THM | bool_sim_false |
|
THM | eq_int_eq_true_intro |
|
THM | eq_int_eq_false_intro |
|
THM | lt_int_eq_true_elim |
|
THM | lt_int_eq_false_elim |
|
THM | eq_atom_eq_true_elim |
|
THM | eq_atom_eq_false_elim |
|
THM | eq_int_eq_true_elim_sqequal |
|
THM | eq_int_eq_false_elim_sqequal |
|
THM | lt_int_eq_true_elim_sqequal |
|
THM | lt_int_eq_false_elim_sqequal |
|
THM | eq_atom_eq_true_elim_sqequal |
|
THM | eq_atom_eq_false_elim_sqequal |
|
THM | bool_cases_sqequal |
|