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 |
![]() ![]() ![]() ![]() ![]() |