definition
- sttfa:set__extensionality/type_0.def
- sttfa:set__extensionality/type_1.def
- sttfa:set__extensionality/type_2.def
- sttfa:set__extensionality/type_3.def
- sttfa:set__extensionality/type_4.def
- sttfa:set__extensionality/term_0.def
- sttfa:set__extensionality/type_5.def
- sttfa:set__extensionality/type_6.def
- sttfa:set__extensionality/term_1.def
- sttfa:set__extensionality/term_2.def
- sttfa:set__extensionality/term_3.def
- sttfa:set__extensionality/type_7.def
- sttfa:set__extensionality/type_8.def
- sttfa:set__extensionality/type_9.def
- sttfa:set__extensionality/type_10.def
- sttfa:set__extensionality/term_4.def
- sttfa:set__extensionality/term_5.def
- sttfa:set__extensionality/term_6.def
- sttfa:set__extensionality/term_7.def
- sttfa:set__extensionality/term_8.def
- sttfa:set__extensionality/term_9.def
- sttfa:set__extensionality/term_10.def
- sttfa:set__extensionality/type_11.def
- sttfa:set__extensionality/type_12.def
- sttfa:set__extensionality/term_11.def
- sttfa:set__extensionality/term_12.def
- sttfa:set__extensionality/term_13.def
- sttfa:set__extensionality/term_14.def
- sttfa:set__extensionality/term_15.def
- sttfa:set__extensionality/term_16.def
- sttfa:set__extensionality/term_17.def
- sttfa:set__extensionality/term_18.def
- sttfa:set__extensionality/term_19.def
- sttfa:set__extensionality/type_13.def
- sttfa:set__extensionality/term_20.def
- sttfa:set__extensionality/term_21.def
- sttfa:set__extensionality/term_22.def
- sttfa:set__extensionality/term_23.def
- sttfa:set__extensionality/term_24.def
- sttfa:set__extensionality/type_14.def
- sttfa:set__extensionality/Set_2Emember.def
- sttfa:set__extensionality/term_25.def
- sttfa:set__extensionality/term_26.def
- sttfa:set__extensionality/term_27.def
- sttfa:set__extensionality/term_28.def
- sttfa:set__extensionality/term_29.def
- sttfa:set__extensionality/term_30.def
- sttfa:set__extensionality/term_31.def
- sttfa:set__extensionality/term_32.def
- sttfa:set__extensionality/term_33.def
- sttfa:set__extensionality/term_34.def
- sttfa:set__extensionality/term_35.def
- sttfa:set__extensionality/term_36.def
- sttfa:set__extensionality/term_37.def
- sttfa:set__extensionality/term_38.def
- sttfa:set__extensionality/term_39.def
- sttfa:set__extensionality/term_40.def
- sttfa:set__extensionality/term_41.def
- sttfa:set__extensionality/type_15.def
- sttfa:set__extensionality/term_42.def
- sttfa:set__extensionality/term_43.def
- sttfa:set__extensionality/term_44.def
- sttfa:set__extensionality/term_45.def
- sttfa:set__extensionality/term_46.def
- sttfa:set__extensionality/term_47.def
- sttfa:set__extensionality/term_48.def
- sttfa:set__extensionality/term_49.def
- sttfa:set__extensionality/term_50.def
- sttfa:set__extensionality/term_51.def
- sttfa:set__extensionality/term_52.def
- sttfa:set__extensionality/term_53.def
- sttfa:set__extensionality/term_54.def
- sttfa:set__extensionality/term_55.def
- sttfa:set__extensionality/term_56.def
- sttfa:set__extensionality/term_57.def
- sttfa:set__extensionality/term_58.def
- sttfa:set__extensionality/type_16.def
- sttfa:set__extensionality/term_59.def
- sttfa:set__extensionality/term_60.def
- sttfa:set__extensionality/term_61.def
- sttfa:set__extensionality/term_62.def
- sttfa:set__extensionality/term_63.def
- sttfa:set__extensionality/term_64.def
- sttfa:set__extensionality/term_65.def
- sttfa:set__extensionality/type_17.def
- sttfa:set__extensionality/term_66.def
- sttfa:set__extensionality/term_67.def
- sttfa:set__extensionality/term_68.def
- sttfa:set__extensionality/term_69.def
- sttfa:set__extensionality/term_70.def
- sttfa:set__extensionality/term_71.def
- sttfa:set__extensionality/term_72.def
- sttfa:set__extensionality/term_73.def
- sttfa:set__extensionality/term_74.def
- sttfa:set__extensionality/term_75.def
- sttfa:set__extensionality/term_76.def
- sttfa:set__extensionality/term_77.def
- sttfa:set__extensionality/term_78.def
- sttfa:set__extensionality/term_79.def
- sttfa:set__extensionality/term_80.def
theorem
- sttfa:set__extensionality/thm_0.thm
- sttfa:set__extensionality/thm_1.thm
- sttfa:set__extensionality/thm_2.thm
- sttfa:set__extensionality/thm_3.thm
- sttfa:set__extensionality/FUN_EQ_THM.thm
- sttfa:set__extensionality/thm_5.thm
- sttfa:set__extensionality/thm_6.thm
- sttfa:set__extensionality/thm_7.thm
- sttfa:set__extensionality/thm_8.thm
- sttfa:set__extensionality/thm_9.thm
- sttfa:set__extensionality/thm_10.thm
- sttfa:set__extensionality/thm_11.thm
- sttfa:set__extensionality/thm_12.thm
- sttfa:set__extensionality/thm_13.thm
- sttfa:set__extensionality/IN.thm
- sttfa:set__extensionality/thm_15.thm
- sttfa:set__extensionality/thm_16.thm
- sttfa:set__extensionality/thm_17.thm
- sttfa:set__extensionality/thm_18.thm
- sttfa:set__extensionality/thm_19.thm
- sttfa:set__extensionality/thm_20.thm
- sttfa:set__extensionality/thm_21.thm
- sttfa:set__extensionality/thm_22.thm
- sttfa:set__extensionality/thm_23.thm
- sttfa:set__extensionality/thm_24.thm
- sttfa:set__extensionality/thm_25.thm
- sttfa:set__extensionality/thm_26.thm
- sttfa:set__extensionality/thm_27.thm
- sttfa:set__extensionality/REFL_CLAUSE.thm
- sttfa:set__extensionality/thm_29.thm
- sttfa:set__extensionality/thm_30.thm
- sttfa:set__extensionality/thm_31.thm
- sttfa:set__extensionality/thm_32.thm
- sttfa:set__extensionality/thm_33.thm
- sttfa:set__extensionality/thm_34.thm
- sttfa:set__extensionality/thm_35.thm
- sttfa:set__extensionality/thm_36.thm
- sttfa:set__extensionality/thm_37.thm
- sttfa:set__extensionality/thm_38.thm
- sttfa:set__extensionality/FORALL_SIMP.thm
- sttfa:set__extensionality/thm_40.thm
- sttfa:set__extensionality/thm_41.thm
- sttfa:set__extensionality/thm_42.thm
- sttfa:set__extensionality/thm_43.thm
- sttfa:set__extensionality/thm_44.thm
- sttfa:set__extensionality/thm_45.thm
- sttfa:set__extensionality/thm_46.thm
- sttfa:set__extensionality/thm_47.thm
- sttfa:set__extensionality/thm_48.thm
- sttfa:set__extensionality/thm_49.thm
- sttfa:set__extensionality/thm_50.thm
- sttfa:set__extensionality/thm_51.thm
- sttfa:set__extensionality/thm_52.thm
- sttfa:set__extensionality/thm_53.thm
- sttfa:set__extensionality/TRUTH.thm
- sttfa:set__extensionality/thm_55.thm
- sttfa:set__extensionality/EXTENSION.thm