blob: 6b406acf5de2263e6917165245de2b39f2f0c979 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
|
1 prop_congr
2 is_true_true
3 not_false_is_true
4 is_true_locked_true
5 negbT
6 negbTE
7 negbF
8 negbFE
9 negbK
10 negbNE
11 negb_inj
12 negbLR
13 negbRL
14 contra
15 contraL
16 contraR
17 contraLR
18 contraT
19 wlog_neg
20 contraFT
21 contraFN
22 contraTF
23 contraNF
24 contraFF
25 ifP
26 ifPn
27 if_same
28 if_neg
29 fun_if
30 if_arg
31 ifE
32 introNTF
33 introTF
34 elimNTF
35 elimTF
36 equivPif
37 xorPif
38 introTFn
39 elimTFn
40 equivPifn
41 xorPifn
42 introT
43 introF
44 introN
45 introNf
46 introTn
47 introFn
48 elimT
49 elimF
50 elimN
51 elimNf
52 elimTn
53 elimFn
54 introP
55 iffP
56 equivP
57 sumboolP
58 appP
59 sameP
60 decPcases
61 rwP
62 rwP2
63 altP
64 bind_unless
65 unless_contra
66 classicP
67 classic_bind
68 classic_EM
69 classic_imply
70 classic_pick
71 all_and2
72 all_and3
73 all_and4
74 all_and5
75 idP
76 boolP
77 idPn
78 negP
79 negPn
80 negPf
81 andP
82 and3P
83 and4P
84 and5P
85 orP
86 or3P
87 or4P
88 nandP
89 norP
90 implyP
91 andTb
92 andFb
93 andbT
94 andbF
95 andbb
96 andbC
97 andbA
98 andbCA
99 andbAC
100 andbACA
101 orTb
102 orFb
103 orbT
104 orbF
105 orbb
106 orbC
107 orbA
108 orbCA
109 orbAC
110 orbACA
111 andbN
112 andNb
113 orbN
114 orNb
115 andb_orl
116 andb_orr
117 orb_andl
118 orb_andr
119 andb_idl
120 andb_idr
121 andb_id2l
122 andb_id2r
123 orb_idl
124 orb_idr
125 orb_id2l
126 orb_id2r
127 negb_and
128 negb_or
129 andbK
130 andKb
131 orbK
132 orKb
133 implybT
134 implybF
135 implyFb
136 implyTb
137 implybb
138 negb_imply
139 implybE
140 implyNb
141 implybN
142 implybNN
143 implyb_idl
144 implyb_idr
145 implyb_id2l
146 addFb
147 addbF
148 addbb
149 addbC
150 addbA
151 addbCA
152 addbAC
153 addbACA
154 andb_addl
155 andb_addr
156 addKb
157 addbK
158 addIb
159 addbI
160 addTb
161 addbT
162 addbN
163 addNb
164 addbP
165 subrelUl
166 subrelUr
167 sub_refl
168 mem_topred
169 topredE
170 app_predE
171 in_applicative
172 in_collective
173 in_simpl
174 unfold_in
175 simpl_predE
176 mem_simpl
177 mem_mem
178 qualifE
179 keyed_predE
180 symmetric_from_pre
181 sym_left_transitive
182 sym_right_transitive
183 equivalence_relP
184 rev_trans
185 forE
186 in1W
187 in2W
188 in3W
189 in1T
190 in2T
191 in3T
192 sub_in1
193 sub_in11
194 sub_in111
195 on1W
196 on1lW
197 on2W
198 on1T
199 on1lT
200 on2T
201 subon1
202 subon1l
203 subon2
204 can_in_inj
205 canLR_in
206 canRL_in
207 on_can_inj
208 canLR_on
209 canRL_on
210 inW_bij
211 onW_bij
212 inT_bij
213 onT_bij
214 sub_in_bij
215 subon_bij
216 sub_in2
217 sub_in3
218 sub_in12
219 sub_in21
220 equivalence_relP_in
221 monoW
222 mono2W
223 homoRL
224 homoLR
225 homo_mono
226 monoLR
227 monoRL
228 can_mono
229 monoW_in
230 mono2W_in
231 homoRL_in
232 homoLR_in
233 homo_mono_in
234 monoLR_in
235 monoRL_in
236 can_mono_in
|
