definition
- sttfa:set__def__a1/type_0.def
- sttfa:set__def__a1/type_1.def
- sttfa:set__def__a1/type_2.def
- sttfa:set__def__a1/term_0.def
- sttfa:set__def__a1/term_1.def
- sttfa:set__def__a1/type_3.def
- sttfa:set__def__a1/term_2.def
- sttfa:set__def__a1/type_4.def
- sttfa:set__def__a1/type_5.def
- sttfa:set__def__a1/Set_2Emember.def
- sttfa:set__def__a1/term_3.def
- sttfa:set__def__a1/term_4.def
- sttfa:set__def__a1/term_5.def
- sttfa:set__def__a1/term_6.def
- sttfa:set__def__a1/term_7.def
- sttfa:set__def__a1/term_8.def
- sttfa:set__def__a1/term_9.def
- sttfa:set__def__a1/Set_2Echoice.def
- sttfa:set__def__a1/term_10.def
- sttfa:set__def__a1/term_11.def
- sttfa:set__def__a1/term_12.def
- sttfa:set__def__a1/term_13.def
- sttfa:set__def__a1/type_6.def
- sttfa:set__def__a1/term_14.def
- sttfa:set__def__a1/type_7.def
- sttfa:set__def__a1/term_15.def
- sttfa:set__def__a1/term_16.def
- sttfa:set__def__a1/term_17.def
- sttfa:set__def__a1/term_18.def
- sttfa:set__def__a1/term_19.def
- sttfa:set__def__a1/term_20.def
- sttfa:set__def__a1/term_21.def
- sttfa:set__def__a1/term_22.def
- sttfa:set__def__a1/type_8.def
- sttfa:set__def__a1/Set_2Edelete.def
- sttfa:set__def__a1/term_23.def
- sttfa:set__def__a1/term_24.def
- sttfa:set__def__a1/term_25.def
- sttfa:set__def__a1/term_26.def
- sttfa:set__def__a1/term_27.def
- sttfa:set__def__a1/Set_2Erest.def
- sttfa:set__def__a1/term_28.def
- sttfa:set__def__a1/term_29.def
- sttfa:set__def__a1/term_30.def
- sttfa:set__def__a1/type_9.def
- sttfa:set__def__a1/term_31.def
- sttfa:set__def__a1/type_10.def
- sttfa:set__def__a1/term_32.def
- sttfa:set__def__a1/term_33.def
- sttfa:set__def__a1/term_34.def
- sttfa:set__def__a1/term_35.def
- sttfa:set__def__a1/term_36.def
- sttfa:set__def__a1/term_37.def
theorem
- sttfa:set__def__a1/thm_0.thm
- sttfa:set__def__a1/thm_1.thm
- sttfa:set__def__a1/thm_2.thm
- sttfa:set__def__a1/thm_3.thm
- sttfa:set__def__a1/thm_4.thm
- sttfa:set__def__a1/thm_5.thm
- sttfa:set__def__a1/thm_6.thm
- sttfa:set__def__a1/thm_7.thm
- sttfa:set__def__a1/thm_8.thm
- sttfa:set__def__a1/thm_9.thm
- sttfa:set__def__a1/thm_10.thm
- sttfa:set__def__a1/CHOICE.thm
- sttfa:set__def__a1/thm_12.thm
- sttfa:set__def__a1/thm_13.thm
- sttfa:set__def__a1/thm_14.thm
- sttfa:set__def__a1/thm_15.thm
- sttfa:set__def__a1/thm_16.thm
- sttfa:set__def__a1/thm_17.thm
- sttfa:set__def__a1/thm_18.thm
- sttfa:set__def__a1/thm_19.thm
- sttfa:set__def__a1/thm_20.thm
- sttfa:set__def__a1/thm_21.thm
- sttfa:set__def__a1/thm_22.thm
- sttfa:set__def__a1/REST.thm