lean4/tests/simpperf/pre2000.lean

axiom f (x : Prop) : Prop
axiom g0 (x : Prop) : Prop
axiom g1 (x : Prop) : Prop
axiom g2 (x : Prop) : Prop
axiom g3 (x : Prop) : Prop
axiom g4 (x : Prop) : Prop
axiom g5 (x : Prop) : Prop
axiom g6 (x : Prop) : Prop
axiom g7 (x : Prop) : Prop
axiom g8 (x : Prop) : Prop
axiom g9 (x : Prop) : Prop
axiom g10 (x : Prop) : Prop
axiom g11 (x : Prop) : Prop
axiom g12 (x : Prop) : Prop
axiom g13 (x : Prop) : Prop
axiom g14 (x : Prop) : Prop
axiom g15 (x : Prop) : Prop
axiom g16 (x : Prop) : Prop
axiom g17 (x : Prop) : Prop
axiom g18 (x : Prop) : Prop
axiom g19 (x : Prop) : Prop
axiom g20 (x : Prop) : Prop
axiom g21 (x : Prop) : Prop
axiom g22 (x : Prop) : Prop
axiom g23 (x : Prop) : Prop
axiom g24 (x : Prop) : Prop
axiom g25 (x : Prop) : Prop
axiom g26 (x : Prop) : Prop
axiom g27 (x : Prop) : Prop
axiom g28 (x : Prop) : Prop
axiom g29 (x : Prop) : Prop
axiom g30 (x : Prop) : Prop
axiom g31 (x : Prop) : Prop
axiom g32 (x : Prop) : Prop
axiom g33 (x : Prop) : Prop
axiom g34 (x : Prop) : Prop
axiom g35 (x : Prop) : Prop
axiom g36 (x : Prop) : Prop
axiom g37 (x : Prop) : Prop
axiom g38 (x : Prop) : Prop
axiom g39 (x : Prop) : Prop
axiom g40 (x : Prop) : Prop
axiom g41 (x : Prop) : Prop
axiom g42 (x : Prop) : Prop
axiom g43 (x : Prop) : Prop
axiom g44 (x : Prop) : Prop
axiom g45 (x : Prop) : Prop
axiom g46 (x : Prop) : Prop
axiom g47 (x : Prop) : Prop
axiom g48 (x : Prop) : Prop
axiom g49 (x : Prop) : Prop
axiom g50 (x : Prop) : Prop
axiom g51 (x : Prop) : Prop
axiom g52 (x : Prop) : Prop
axiom g53 (x : Prop) : Prop
axiom g54 (x : Prop) : Prop
axiom g55 (x : Prop) : Prop
axiom g56 (x : Prop) : Prop
axiom g57 (x : Prop) : Prop
axiom g58 (x : Prop) : Prop
axiom g59 (x : Prop) : Prop
axiom g60 (x : Prop) : Prop
axiom g61 (x : Prop) : Prop
axiom g62 (x : Prop) : Prop
axiom g63 (x : Prop) : Prop
axiom g64 (x : Prop) : Prop
axiom g65 (x : Prop) : Prop
axiom g66 (x : Prop) : Prop
axiom g67 (x : Prop) : Prop
axiom g68 (x : Prop) : Prop
axiom g69 (x : Prop) : Prop
axiom g70 (x : Prop) : Prop
axiom g71 (x : Prop) : Prop
axiom g72 (x : Prop) : Prop
axiom g73 (x : Prop) : Prop
axiom g74 (x : Prop) : Prop
axiom g75 (x : Prop) : Prop
axiom g76 (x : Prop) : Prop
axiom g77 (x : Prop) : Prop
axiom g78 (x : Prop) : Prop
axiom g79 (x : Prop) : Prop
axiom g80 (x : Prop) : Prop
axiom g81 (x : Prop) : Prop
axiom g82 (x : Prop) : Prop
axiom g83 (x : Prop) : Prop
axiom g84 (x : Prop) : Prop
axiom g85 (x : Prop) : Prop
axiom g86 (x : Prop) : Prop
axiom g87 (x : Prop) : Prop
axiom g88 (x : Prop) : Prop
axiom g89 (x : Prop) : Prop
axiom g90 (x : Prop) : Prop
axiom g91 (x : Prop) : Prop
axiom g92 (x : Prop) : Prop
axiom g93 (x : Prop) : Prop
axiom g94 (x : Prop) : Prop
axiom g95 (x : Prop) : Prop
axiom g96 (x : Prop) : Prop
axiom g97 (x : Prop) : Prop
axiom g98 (x : Prop) : Prop
axiom g99 (x : Prop) : Prop
axiom g100 (x : Prop) : Prop
axiom g101 (x : Prop) : Prop
axiom g102 (x : Prop) : Prop
axiom g103 (x : Prop) : Prop
axiom g104 (x : Prop) : Prop
axiom g105 (x : Prop) : Prop
axiom g106 (x : Prop) : Prop
axiom g107 (x : Prop) : Prop
axiom g108 (x : Prop) : Prop
axiom g109 (x : Prop) : Prop
axiom g110 (x : Prop) : Prop
axiom g111 (x : Prop) : Prop
axiom g112 (x : Prop) : Prop
axiom g113 (x : Prop) : Prop
axiom g114 (x : Prop) : Prop
axiom g115 (x : Prop) : Prop
axiom g116 (x : Prop) : Prop
axiom g117 (x : Prop) : Prop
axiom g118 (x : Prop) : Prop
axiom g119 (x : Prop) : Prop
axiom g120 (x : Prop) : Prop
axiom g121 (x : Prop) : Prop
axiom g122 (x : Prop) : Prop
axiom g123 (x : Prop) : Prop
axiom g124 (x : Prop) : Prop
axiom g125 (x : Prop) : Prop
axiom g126 (x : Prop) : Prop
axiom g127 (x : Prop) : Prop
axiom g128 (x : Prop) : Prop
axiom g129 (x : Prop) : Prop
axiom g130 (x : Prop) : Prop
axiom g131 (x : Prop) : Prop
axiom g132 (x : Prop) : Prop
axiom g133 (x : Prop) : Prop
axiom g134 (x : Prop) : Prop
axiom g135 (x : Prop) : Prop
axiom g136 (x : Prop) : Prop
axiom g137 (x : Prop) : Prop
axiom g138 (x : Prop) : Prop
axiom g139 (x : Prop) : Prop
axiom g140 (x : Prop) : Prop
axiom g141 (x : Prop) : Prop
axiom g142 (x : Prop) : Prop
axiom g143 (x : Prop) : Prop
axiom g144 (x : Prop) : Prop
axiom g145 (x : Prop) : Prop
axiom g146 (x : Prop) : Prop
axiom g147 (x : Prop) : Prop
axiom g148 (x : Prop) : Prop
axiom g149 (x : Prop) : Prop
axiom g150 (x : Prop) : Prop
axiom g151 (x : Prop) : Prop
axiom g152 (x : Prop) : Prop
axiom g153 (x : Prop) : Prop
axiom g154 (x : Prop) : Prop
axiom g155 (x : Prop) : Prop
axiom g156 (x : Prop) : Prop
axiom g157 (x : Prop) : Prop
axiom g158 (x : Prop) : Prop
axiom g159 (x : Prop) : Prop
axiom g160 (x : Prop) : Prop
axiom g161 (x : Prop) : Prop
axiom g162 (x : Prop) : Prop
axiom g163 (x : Prop) : Prop
axiom g164 (x : Prop) : Prop
axiom g165 (x : Prop) : Prop
axiom g166 (x : Prop) : Prop
axiom g167 (x : Prop) : Prop
axiom g168 (x : Prop) : Prop
axiom g169 (x : Prop) : Prop
axiom g170 (x : Prop) : Prop
axiom g171 (x : Prop) : Prop
axiom g172 (x : Prop) : Prop
axiom g173 (x : Prop) : Prop
axiom g174 (x : Prop) : Prop
axiom g175 (x : Prop) : Prop
axiom g176 (x : Prop) : Prop
axiom g177 (x : Prop) : Prop
axiom g178 (x : Prop) : Prop
axiom g179 (x : Prop) : Prop
axiom g180 (x : Prop) : Prop
axiom g181 (x : Prop) : Prop
axiom g182 (x : Prop) : Prop
axiom g183 (x : Prop) : Prop
axiom g184 (x : Prop) : Prop
axiom g185 (x : Prop) : Prop
axiom g186 (x : Prop) : Prop
axiom g187 (x : Prop) : Prop
axiom g188 (x : Prop) : Prop
axiom g189 (x : Prop) : Prop
axiom g190 (x : Prop) : Prop
axiom g191 (x : Prop) : Prop
axiom g192 (x : Prop) : Prop
axiom g193 (x : Prop) : Prop
axiom g194 (x : Prop) : Prop
axiom g195 (x : Prop) : Prop
axiom g196 (x : Prop) : Prop
axiom g197 (x : Prop) : Prop
axiom g198 (x : Prop) : Prop
axiom g199 (x : Prop) : Prop
axiom g200 (x : Prop) : Prop
axiom g201 (x : Prop) : Prop
axiom g202 (x : Prop) : Prop
axiom g203 (x : Prop) : Prop
axiom g204 (x : Prop) : Prop
axiom g205 (x : Prop) : Prop
axiom g206 (x : Prop) : Prop
axiom g207 (x : Prop) : Prop
axiom g208 (x : Prop) : Prop
axiom g209 (x : Prop) : Prop
axiom g210 (x : Prop) : Prop
axiom g211 (x : Prop) : Prop
axiom g212 (x : Prop) : Prop
axiom g213 (x : Prop) : Prop
axiom g214 (x : Prop) : Prop
axiom g215 (x : Prop) : Prop
axiom g216 (x : Prop) : Prop
axiom g217 (x : Prop) : Prop
axiom g218 (x : Prop) : Prop
axiom g219 (x : Prop) : Prop
axiom g220 (x : Prop) : Prop
axiom g221 (x : Prop) : Prop
axiom g222 (x : Prop) : Prop
axiom g223 (x : Prop) : Prop
axiom g224 (x : Prop) : Prop
axiom g225 (x : Prop) : Prop
axiom g226 (x : Prop) : Prop
axiom g227 (x : Prop) : Prop
axiom g228 (x : Prop) : Prop
axiom g229 (x : Prop) : Prop
axiom g230 (x : Prop) : Prop
axiom g231 (x : Prop) : Prop
axiom g232 (x : Prop) : Prop
axiom g233 (x : Prop) : Prop
axiom g234 (x : Prop) : Prop
axiom g235 (x : Prop) : Prop
axiom g236 (x : Prop) : Prop
axiom g237 (x : Prop) : Prop
axiom g238 (x : Prop) : Prop
axiom g239 (x : Prop) : Prop
axiom g240 (x : Prop) : Prop
axiom g241 (x : Prop) : Prop
axiom g242 (x : Prop) : Prop
axiom g243 (x : Prop) : Prop
axiom g244 (x : Prop) : Prop
axiom g245 (x : Prop) : Prop
axiom g246 (x : Prop) : Prop
axiom g247 (x : Prop) : Prop
axiom g248 (x : Prop) : Prop
axiom g249 (x : Prop) : Prop
axiom g250 (x : Prop) : Prop
axiom g251 (x : Prop) : Prop
axiom g252 (x : Prop) : Prop
axiom g253 (x : Prop) : Prop
axiom g254 (x : Prop) : Prop
axiom g255 (x : Prop) : Prop
axiom g256 (x : Prop) : Prop
axiom g257 (x : Prop) : Prop
axiom g258 (x : Prop) : Prop
axiom g259 (x : Prop) : Prop
axiom g260 (x : Prop) : Prop
axiom g261 (x : Prop) : Prop
axiom g262 (x : Prop) : Prop
axiom g263 (x : Prop) : Prop
axiom g264 (x : Prop) : Prop
axiom g265 (x : Prop) : Prop
axiom g266 (x : Prop) : Prop
axiom g267 (x : Prop) : Prop
axiom g268 (x : Prop) : Prop
axiom g269 (x : Prop) : Prop
axiom g270 (x : Prop) : Prop
axiom g271 (x : Prop) : Prop
axiom g272 (x : Prop) : Prop
axiom g273 (x : Prop) : Prop
axiom g274 (x : Prop) : Prop
axiom g275 (x : Prop) : Prop
axiom g276 (x : Prop) : Prop
axiom g277 (x : Prop) : Prop
axiom g278 (x : Prop) : Prop
axiom g279 (x : Prop) : Prop
axiom g280 (x : Prop) : Prop
axiom g281 (x : Prop) : Prop
axiom g282 (x : Prop) : Prop
axiom g283 (x : Prop) : Prop
axiom g284 (x : Prop) : Prop
axiom g285 (x : Prop) : Prop
axiom g286 (x : Prop) : Prop
axiom g287 (x : Prop) : Prop
axiom g288 (x : Prop) : Prop
axiom g289 (x : Prop) : Prop
axiom g290 (x : Prop) : Prop
axiom g291 (x : Prop) : Prop
axiom g292 (x : Prop) : Prop
axiom g293 (x : Prop) : Prop
axiom g294 (x : Prop) : Prop
axiom g295 (x : Prop) : Prop
axiom g296 (x : Prop) : Prop
axiom g297 (x : Prop) : Prop
axiom g298 (x : Prop) : Prop
axiom g299 (x : Prop) : Prop
axiom g300 (x : Prop) : Prop
axiom g301 (x : Prop) : Prop
axiom g302 (x : Prop) : Prop
axiom g303 (x : Prop) : Prop
axiom g304 (x : Prop) : Prop
axiom g305 (x : Prop) : Prop
axiom g306 (x : Prop) : Prop
axiom g307 (x : Prop) : Prop
axiom g308 (x : Prop) : Prop
axiom g309 (x : Prop) : Prop
axiom g310 (x : Prop) : Prop
axiom g311 (x : Prop) : Prop
axiom g312 (x : Prop) : Prop
axiom g313 (x : Prop) : Prop
axiom g314 (x : Prop) : Prop
axiom g315 (x : Prop) : Prop
axiom g316 (x : Prop) : Prop
axiom g317 (x : Prop) : Prop
axiom g318 (x : Prop) : Prop
axiom g319 (x : Prop) : Prop
axiom g320 (x : Prop) : Prop
axiom g321 (x : Prop) : Prop
axiom g322 (x : Prop) : Prop
axiom g323 (x : Prop) : Prop
axiom g324 (x : Prop) : Prop
axiom g325 (x : Prop) : Prop
axiom g326 (x : Prop) : Prop
axiom g327 (x : Prop) : Prop
axiom g328 (x : Prop) : Prop
axiom g329 (x : Prop) : Prop
axiom g330 (x : Prop) : Prop
axiom g331 (x : Prop) : Prop
axiom g332 (x : Prop) : Prop
axiom g333 (x : Prop) : Prop
axiom g334 (x : Prop) : Prop
axiom g335 (x : Prop) : Prop
axiom g336 (x : Prop) : Prop
axiom g337 (x : Prop) : Prop
axiom g338 (x : Prop) : Prop
axiom g339 (x : Prop) : Prop
axiom g340 (x : Prop) : Prop
axiom g341 (x : Prop) : Prop
axiom g342 (x : Prop) : Prop
axiom g343 (x : Prop) : Prop
axiom g344 (x : Prop) : Prop
axiom g345 (x : Prop) : Prop
axiom g346 (x : Prop) : Prop
axiom g347 (x : Prop) : Prop
axiom g348 (x : Prop) : Prop
axiom g349 (x : Prop) : Prop
axiom g350 (x : Prop) : Prop
axiom g351 (x : Prop) : Prop
axiom g352 (x : Prop) : Prop
axiom g353 (x : Prop) : Prop
axiom g354 (x : Prop) : Prop
axiom g355 (x : Prop) : Prop
axiom g356 (x : Prop) : Prop
axiom g357 (x : Prop) : Prop
axiom g358 (x : Prop) : Prop
axiom g359 (x : Prop) : Prop
axiom g360 (x : Prop) : Prop
axiom g361 (x : Prop) : Prop
axiom g362 (x : Prop) : Prop
axiom g363 (x : Prop) : Prop
axiom g364 (x : Prop) : Prop
axiom g365 (x : Prop) : Prop
axiom g366 (x : Prop) : Prop
axiom g367 (x : Prop) : Prop
axiom g368 (x : Prop) : Prop
axiom g369 (x : Prop) : Prop
axiom g370 (x : Prop) : Prop
axiom g371 (x : Prop) : Prop
axiom g372 (x : Prop) : Prop
axiom g373 (x : Prop) : Prop
axiom g374 (x : Prop) : Prop
axiom g375 (x : Prop) : Prop
axiom g376 (x : Prop) : Prop
axiom g377 (x : Prop) : Prop
axiom g378 (x : Prop) : Prop
axiom g379 (x : Prop) : Prop
axiom g380 (x : Prop) : Prop
axiom g381 (x : Prop) : Prop
axiom g382 (x : Prop) : Prop
axiom g383 (x : Prop) : Prop
axiom g384 (x : Prop) : Prop
axiom g385 (x : Prop) : Prop
axiom g386 (x : Prop) : Prop
axiom g387 (x : Prop) : Prop
axiom g388 (x : Prop) : Prop
axiom g389 (x : Prop) : Prop
axiom g390 (x : Prop) : Prop
axiom g391 (x : Prop) : Prop
axiom g392 (x : Prop) : Prop
axiom g393 (x : Prop) : Prop
axiom g394 (x : Prop) : Prop
axiom g395 (x : Prop) : Prop
axiom g396 (x : Prop) : Prop
axiom g397 (x : Prop) : Prop
axiom g398 (x : Prop) : Prop
axiom g399 (x : Prop) : Prop
axiom g400 (x : Prop) : Prop
axiom g401 (x : Prop) : Prop
axiom g402 (x : Prop) : Prop
axiom g403 (x : Prop) : Prop
axiom g404 (x : Prop) : Prop
axiom g405 (x : Prop) : Prop
axiom g406 (x : Prop) : Prop
axiom g407 (x : Prop) : Prop
axiom g408 (x : Prop) : Prop
axiom g409 (x : Prop) : Prop
axiom g410 (x : Prop) : Prop
axiom g411 (x : Prop) : Prop
axiom g412 (x : Prop) : Prop
axiom g413 (x : Prop) : Prop
axiom g414 (x : Prop) : Prop
axiom g415 (x : Prop) : Prop
axiom g416 (x : Prop) : Prop
axiom g417 (x : Prop) : Prop
axiom g418 (x : Prop) : Prop
axiom g419 (x : Prop) : Prop
axiom g420 (x : Prop) : Prop
axiom g421 (x : Prop) : Prop
axiom g422 (x : Prop) : Prop
axiom g423 (x : Prop) : Prop
axiom g424 (x : Prop) : Prop
axiom g425 (x : Prop) : Prop
axiom g426 (x : Prop) : Prop
axiom g427 (x : Prop) : Prop
axiom g428 (x : Prop) : Prop
axiom g429 (x : Prop) : Prop
axiom g430 (x : Prop) : Prop
axiom g431 (x : Prop) : Prop
axiom g432 (x : Prop) : Prop
axiom g433 (x : Prop) : Prop
axiom g434 (x : Prop) : Prop
axiom g435 (x : Prop) : Prop
axiom g436 (x : Prop) : Prop
axiom g437 (x : Prop) : Prop
axiom g438 (x : Prop) : Prop
axiom g439 (x : Prop) : Prop
axiom g440 (x : Prop) : Prop
axiom g441 (x : Prop) : Prop
axiom g442 (x : Prop) : Prop
axiom g443 (x : Prop) : Prop
axiom g444 (x : Prop) : Prop
axiom g445 (x : Prop) : Prop
axiom g446 (x : Prop) : Prop
axiom g447 (x : Prop) : Prop
axiom g448 (x : Prop) : Prop
axiom g449 (x : Prop) : Prop
axiom g450 (x : Prop) : Prop
axiom g451 (x : Prop) : Prop
axiom g452 (x : Prop) : Prop
axiom g453 (x : Prop) : Prop
axiom g454 (x : Prop) : Prop
axiom g455 (x : Prop) : Prop
axiom g456 (x : Prop) : Prop
axiom g457 (x : Prop) : Prop
axiom g458 (x : Prop) : Prop
axiom g459 (x : Prop) : Prop
axiom g460 (x : Prop) : Prop
axiom g461 (x : Prop) : Prop
axiom g462 (x : Prop) : Prop
axiom g463 (x : Prop) : Prop
axiom g464 (x : Prop) : Prop
axiom g465 (x : Prop) : Prop
axiom g466 (x : Prop) : Prop
axiom g467 (x : Prop) : Prop
axiom g468 (x : Prop) : Prop
axiom g469 (x : Prop) : Prop
axiom g470 (x : Prop) : Prop
axiom g471 (x : Prop) : Prop
axiom g472 (x : Prop) : Prop
axiom g473 (x : Prop) : Prop
axiom g474 (x : Prop) : Prop
axiom g475 (x : Prop) : Prop
axiom g476 (x : Prop) : Prop
axiom g477 (x : Prop) : Prop
axiom g478 (x : Prop) : Prop
axiom g479 (x : Prop) : Prop
axiom g480 (x : Prop) : Prop
axiom g481 (x : Prop) : Prop
axiom g482 (x : Prop) : Prop
axiom g483 (x : Prop) : Prop
axiom g484 (x : Prop) : Prop
axiom g485 (x : Prop) : Prop
axiom g486 (x : Prop) : Prop
axiom g487 (x : Prop) : Prop
axiom g488 (x : Prop) : Prop
axiom g489 (x : Prop) : Prop
axiom g490 (x : Prop) : Prop
axiom g491 (x : Prop) : Prop
axiom g492 (x : Prop) : Prop
axiom g493 (x : Prop) : Prop
axiom g494 (x : Prop) : Prop
axiom g495 (x : Prop) : Prop
axiom g496 (x : Prop) : Prop
axiom g497 (x : Prop) : Prop
axiom g498 (x : Prop) : Prop
axiom g499 (x : Prop) : Prop
axiom g500 (x : Prop) : Prop
axiom g501 (x : Prop) : Prop
axiom g502 (x : Prop) : Prop
axiom g503 (x : Prop) : Prop
axiom g504 (x : Prop) : Prop
axiom g505 (x : Prop) : Prop
axiom g506 (x : Prop) : Prop
axiom g507 (x : Prop) : Prop
axiom g508 (x : Prop) : Prop
axiom g509 (x : Prop) : Prop
axiom g510 (x : Prop) : Prop
axiom g511 (x : Prop) : Prop
axiom g512 (x : Prop) : Prop
axiom g513 (x : Prop) : Prop
axiom g514 (x : Prop) : Prop
axiom g515 (x : Prop) : Prop
axiom g516 (x : Prop) : Prop
axiom g517 (x : Prop) : Prop
axiom g518 (x : Prop) : Prop
axiom g519 (x : Prop) : Prop
axiom g520 (x : Prop) : Prop
axiom g521 (x : Prop) : Prop
axiom g522 (x : Prop) : Prop
axiom g523 (x : Prop) : Prop
axiom g524 (x : Prop) : Prop
axiom g525 (x : Prop) : Prop
axiom g526 (x : Prop) : Prop
axiom g527 (x : Prop) : Prop
axiom g528 (x : Prop) : Prop
axiom g529 (x : Prop) : Prop
axiom g530 (x : Prop) : Prop
axiom g531 (x : Prop) : Prop
axiom g532 (x : Prop) : Prop
axiom g533 (x : Prop) : Prop
axiom g534 (x : Prop) : Prop
axiom g535 (x : Prop) : Prop
axiom g536 (x : Prop) : Prop
axiom g537 (x : Prop) : Prop
axiom g538 (x : Prop) : Prop
axiom g539 (x : Prop) : Prop
axiom g540 (x : Prop) : Prop
axiom g541 (x : Prop) : Prop
axiom g542 (x : Prop) : Prop
axiom g543 (x : Prop) : Prop
axiom g544 (x : Prop) : Prop
axiom g545 (x : Prop) : Prop
axiom g546 (x : Prop) : Prop
axiom g547 (x : Prop) : Prop
axiom g548 (x : Prop) : Prop
axiom g549 (x : Prop) : Prop
axiom g550 (x : Prop) : Prop
axiom g551 (x : Prop) : Prop
axiom g552 (x : Prop) : Prop
axiom g553 (x : Prop) : Prop
axiom g554 (x : Prop) : Prop
axiom g555 (x : Prop) : Prop
axiom g556 (x : Prop) : Prop
axiom g557 (x : Prop) : Prop
axiom g558 (x : Prop) : Prop
axiom g559 (x : Prop) : Prop
axiom g560 (x : Prop) : Prop
axiom g561 (x : Prop) : Prop
axiom g562 (x : Prop) : Prop
axiom g563 (x : Prop) : Prop
axiom g564 (x : Prop) : Prop
axiom g565 (x : Prop) : Prop
axiom g566 (x : Prop) : Prop
axiom g567 (x : Prop) : Prop
axiom g568 (x : Prop) : Prop
axiom g569 (x : Prop) : Prop
axiom g570 (x : Prop) : Prop
axiom g571 (x : Prop) : Prop
axiom g572 (x : Prop) : Prop
axiom g573 (x : Prop) : Prop
axiom g574 (x : Prop) : Prop
axiom g575 (x : Prop) : Prop
axiom g576 (x : Prop) : Prop
axiom g577 (x : Prop) : Prop
axiom g578 (x : Prop) : Prop
axiom g579 (x : Prop) : Prop
axiom g580 (x : Prop) : Prop
axiom g581 (x : Prop) : Prop
axiom g582 (x : Prop) : Prop
axiom g583 (x : Prop) : Prop
axiom g584 (x : Prop) : Prop
axiom g585 (x : Prop) : Prop
axiom g586 (x : Prop) : Prop
axiom g587 (x : Prop) : Prop
axiom g588 (x : Prop) : Prop
axiom g589 (x : Prop) : Prop
axiom g590 (x : Prop) : Prop
axiom g591 (x : Prop) : Prop
axiom g592 (x : Prop) : Prop
axiom g593 (x : Prop) : Prop
axiom g594 (x : Prop) : Prop
axiom g595 (x : Prop) : Prop
axiom g596 (x : Prop) : Prop
axiom g597 (x : Prop) : Prop
axiom g598 (x : Prop) : Prop
axiom g599 (x : Prop) : Prop
axiom g600 (x : Prop) : Prop
axiom g601 (x : Prop) : Prop
axiom g602 (x : Prop) : Prop
axiom g603 (x : Prop) : Prop
axiom g604 (x : Prop) : Prop
axiom g605 (x : Prop) : Prop
axiom g606 (x : Prop) : Prop
axiom g607 (x : Prop) : Prop
axiom g608 (x : Prop) : Prop
axiom g609 (x : Prop) : Prop
axiom g610 (x : Prop) : Prop
axiom g611 (x : Prop) : Prop
axiom g612 (x : Prop) : Prop
axiom g613 (x : Prop) : Prop
axiom g614 (x : Prop) : Prop
axiom g615 (x : Prop) : Prop
axiom g616 (x : Prop) : Prop
axiom g617 (x : Prop) : Prop
axiom g618 (x : Prop) : Prop
axiom g619 (x : Prop) : Prop
axiom g620 (x : Prop) : Prop
axiom g621 (x : Prop) : Prop
axiom g622 (x : Prop) : Prop
axiom g623 (x : Prop) : Prop
axiom g624 (x : Prop) : Prop
axiom g625 (x : Prop) : Prop
axiom g626 (x : Prop) : Prop
axiom g627 (x : Prop) : Prop
axiom g628 (x : Prop) : Prop
axiom g629 (x : Prop) : Prop
axiom g630 (x : Prop) : Prop
axiom g631 (x : Prop) : Prop
axiom g632 (x : Prop) : Prop
axiom g633 (x : Prop) : Prop
axiom g634 (x : Prop) : Prop
axiom g635 (x : Prop) : Prop
axiom g636 (x : Prop) : Prop
axiom g637 (x : Prop) : Prop
axiom g638 (x : Prop) : Prop
axiom g639 (x : Prop) : Prop
axiom g640 (x : Prop) : Prop
axiom g641 (x : Prop) : Prop
axiom g642 (x : Prop) : Prop
axiom g643 (x : Prop) : Prop
axiom g644 (x : Prop) : Prop
axiom g645 (x : Prop) : Prop
axiom g646 (x : Prop) : Prop
axiom g647 (x : Prop) : Prop
axiom g648 (x : Prop) : Prop
axiom g649 (x : Prop) : Prop
axiom g650 (x : Prop) : Prop
axiom g651 (x : Prop) : Prop
axiom g652 (x : Prop) : Prop
axiom g653 (x : Prop) : Prop
axiom g654 (x : Prop) : Prop
axiom g655 (x : Prop) : Prop
axiom g656 (x : Prop) : Prop
axiom g657 (x : Prop) : Prop
axiom g658 (x : Prop) : Prop
axiom g659 (x : Prop) : Prop
axiom g660 (x : Prop) : Prop
axiom g661 (x : Prop) : Prop
axiom g662 (x : Prop) : Prop
axiom g663 (x : Prop) : Prop
axiom g664 (x : Prop) : Prop
axiom g665 (x : Prop) : Prop
axiom g666 (x : Prop) : Prop
axiom g667 (x : Prop) : Prop
axiom g668 (x : Prop) : Prop
axiom g669 (x : Prop) : Prop
axiom g670 (x : Prop) : Prop
axiom g671 (x : Prop) : Prop
axiom g672 (x : Prop) : Prop
axiom g673 (x : Prop) : Prop
axiom g674 (x : Prop) : Prop
axiom g675 (x : Prop) : Prop
axiom g676 (x : Prop) : Prop
axiom g677 (x : Prop) : Prop
axiom g678 (x : Prop) : Prop
axiom g679 (x : Prop) : Prop
axiom g680 (x : Prop) : Prop
axiom g681 (x : Prop) : Prop
axiom g682 (x : Prop) : Prop
axiom g683 (x : Prop) : Prop
axiom g684 (x : Prop) : Prop
axiom g685 (x : Prop) : Prop
axiom g686 (x : Prop) : Prop
axiom g687 (x : Prop) : Prop
axiom g688 (x : Prop) : Prop
axiom g689 (x : Prop) : Prop
axiom g690 (x : Prop) : Prop
axiom g691 (x : Prop) : Prop
axiom g692 (x : Prop) : Prop
axiom g693 (x : Prop) : Prop
axiom g694 (x : Prop) : Prop
axiom g695 (x : Prop) : Prop
axiom g696 (x : Prop) : Prop
axiom g697 (x : Prop) : Prop
axiom g698 (x : Prop) : Prop
axiom g699 (x : Prop) : Prop
axiom g700 (x : Prop) : Prop
axiom g701 (x : Prop) : Prop
axiom g702 (x : Prop) : Prop
axiom g703 (x : Prop) : Prop
axiom g704 (x : Prop) : Prop
axiom g705 (x : Prop) : Prop
axiom g706 (x : Prop) : Prop
axiom g707 (x : Prop) : Prop
axiom g708 (x : Prop) : Prop
axiom g709 (x : Prop) : Prop
axiom g710 (x : Prop) : Prop
axiom g711 (x : Prop) : Prop
axiom g712 (x : Prop) : Prop
axiom g713 (x : Prop) : Prop
axiom g714 (x : Prop) : Prop
axiom g715 (x : Prop) : Prop
axiom g716 (x : Prop) : Prop
axiom g717 (x : Prop) : Prop
axiom g718 (x : Prop) : Prop
axiom g719 (x : Prop) : Prop
axiom g720 (x : Prop) : Prop
axiom g721 (x : Prop) : Prop
axiom g722 (x : Prop) : Prop
axiom g723 (x : Prop) : Prop
axiom g724 (x : Prop) : Prop
axiom g725 (x : Prop) : Prop
axiom g726 (x : Prop) : Prop
axiom g727 (x : Prop) : Prop
axiom g728 (x : Prop) : Prop
axiom g729 (x : Prop) : Prop
axiom g730 (x : Prop) : Prop
axiom g731 (x : Prop) : Prop
axiom g732 (x : Prop) : Prop
axiom g733 (x : Prop) : Prop
axiom g734 (x : Prop) : Prop
axiom g735 (x : Prop) : Prop
axiom g736 (x : Prop) : Prop
axiom g737 (x : Prop) : Prop
axiom g738 (x : Prop) : Prop
axiom g739 (x : Prop) : Prop
axiom g740 (x : Prop) : Prop
axiom g741 (x : Prop) : Prop
axiom g742 (x : Prop) : Prop
axiom g743 (x : Prop) : Prop
axiom g744 (x : Prop) : Prop
axiom g745 (x : Prop) : Prop
axiom g746 (x : Prop) : Prop
axiom g747 (x : Prop) : Prop
axiom g748 (x : Prop) : Prop
axiom g749 (x : Prop) : Prop
axiom g750 (x : Prop) : Prop
axiom g751 (x : Prop) : Prop
axiom g752 (x : Prop) : Prop
axiom g753 (x : Prop) : Prop
axiom g754 (x : Prop) : Prop
axiom g755 (x : Prop) : Prop
axiom g756 (x : Prop) : Prop
axiom g757 (x : Prop) : Prop
axiom g758 (x : Prop) : Prop
axiom g759 (x : Prop) : Prop
axiom g760 (x : Prop) : Prop
axiom g761 (x : Prop) : Prop
axiom g762 (x : Prop) : Prop
axiom g763 (x : Prop) : Prop
axiom g764 (x : Prop) : Prop
axiom g765 (x : Prop) : Prop
axiom g766 (x : Prop) : Prop
axiom g767 (x : Prop) : Prop
axiom g768 (x : Prop) : Prop
axiom g769 (x : Prop) : Prop
axiom g770 (x : Prop) : Prop
axiom g771 (x : Prop) : Prop
axiom g772 (x : Prop) : Prop
axiom g773 (x : Prop) : Prop
axiom g774 (x : Prop) : Prop
axiom g775 (x : Prop) : Prop
axiom g776 (x : Prop) : Prop
axiom g777 (x : Prop) : Prop
axiom g778 (x : Prop) : Prop
axiom g779 (x : Prop) : Prop
axiom g780 (x : Prop) : Prop
axiom g781 (x : Prop) : Prop
axiom g782 (x : Prop) : Prop
axiom g783 (x : Prop) : Prop
axiom g784 (x : Prop) : Prop
axiom g785 (x : Prop) : Prop
axiom g786 (x : Prop) : Prop
axiom g787 (x : Prop) : Prop
axiom g788 (x : Prop) : Prop
axiom g789 (x : Prop) : Prop
axiom g790 (x : Prop) : Prop
axiom g791 (x : Prop) : Prop
axiom g792 (x : Prop) : Prop
axiom g793 (x : Prop) : Prop
axiom g794 (x : Prop) : Prop
axiom g795 (x : Prop) : Prop
axiom g796 (x : Prop) : Prop
axiom g797 (x : Prop) : Prop
axiom g798 (x : Prop) : Prop
axiom g799 (x : Prop) : Prop
axiom g800 (x : Prop) : Prop
axiom g801 (x : Prop) : Prop
axiom g802 (x : Prop) : Prop
axiom g803 (x : Prop) : Prop
axiom g804 (x : Prop) : Prop
axiom g805 (x : Prop) : Prop
axiom g806 (x : Prop) : Prop
axiom g807 (x : Prop) : Prop
axiom g808 (x : Prop) : Prop
axiom g809 (x : Prop) : Prop
axiom g810 (x : Prop) : Prop
axiom g811 (x : Prop) : Prop
axiom g812 (x : Prop) : Prop
axiom g813 (x : Prop) : Prop
axiom g814 (x : Prop) : Prop
axiom g815 (x : Prop) : Prop
axiom g816 (x : Prop) : Prop
axiom g817 (x : Prop) : Prop
axiom g818 (x : Prop) : Prop
axiom g819 (x : Prop) : Prop
axiom g820 (x : Prop) : Prop
axiom g821 (x : Prop) : Prop
axiom g822 (x : Prop) : Prop
axiom g823 (x : Prop) : Prop
axiom g824 (x : Prop) : Prop
axiom g825 (x : Prop) : Prop
axiom g826 (x : Prop) : Prop
axiom g827 (x : Prop) : Prop
axiom g828 (x : Prop) : Prop
axiom g829 (x : Prop) : Prop
axiom g830 (x : Prop) : Prop
axiom g831 (x : Prop) : Prop
axiom g832 (x : Prop) : Prop
axiom g833 (x : Prop) : Prop
axiom g834 (x : Prop) : Prop
axiom g835 (x : Prop) : Prop
axiom g836 (x : Prop) : Prop
axiom g837 (x : Prop) : Prop
axiom g838 (x : Prop) : Prop
axiom g839 (x : Prop) : Prop
axiom g840 (x : Prop) : Prop
axiom g841 (x : Prop) : Prop
axiom g842 (x : Prop) : Prop
axiom g843 (x : Prop) : Prop
axiom g844 (x : Prop) : Prop
axiom g845 (x : Prop) : Prop
axiom g846 (x : Prop) : Prop
axiom g847 (x : Prop) : Prop
axiom g848 (x : Prop) : Prop
axiom g849 (x : Prop) : Prop
axiom g850 (x : Prop) : Prop
axiom g851 (x : Prop) : Prop
axiom g852 (x : Prop) : Prop
axiom g853 (x : Prop) : Prop
axiom g854 (x : Prop) : Prop
axiom g855 (x : Prop) : Prop
axiom g856 (x : Prop) : Prop
axiom g857 (x : Prop) : Prop
axiom g858 (x : Prop) : Prop
axiom g859 (x : Prop) : Prop
axiom g860 (x : Prop) : Prop
axiom g861 (x : Prop) : Prop
axiom g862 (x : Prop) : Prop
axiom g863 (x : Prop) : Prop
axiom g864 (x : Prop) : Prop
axiom g865 (x : Prop) : Prop
axiom g866 (x : Prop) : Prop
axiom g867 (x : Prop) : Prop
axiom g868 (x : Prop) : Prop
axiom g869 (x : Prop) : Prop
axiom g870 (x : Prop) : Prop
axiom g871 (x : Prop) : Prop
axiom g872 (x : Prop) : Prop
axiom g873 (x : Prop) : Prop
axiom g874 (x : Prop) : Prop
axiom g875 (x : Prop) : Prop
axiom g876 (x : Prop) : Prop
axiom g877 (x : Prop) : Prop
axiom g878 (x : Prop) : Prop
axiom g879 (x : Prop) : Prop
axiom g880 (x : Prop) : Prop
axiom g881 (x : Prop) : Prop
axiom g882 (x : Prop) : Prop
axiom g883 (x : Prop) : Prop
axiom g884 (x : Prop) : Prop
axiom g885 (x : Prop) : Prop
axiom g886 (x : Prop) : Prop
axiom g887 (x : Prop) : Prop
axiom g888 (x : Prop) : Prop
axiom g889 (x : Prop) : Prop
axiom g890 (x : Prop) : Prop
axiom g891 (x : Prop) : Prop
axiom g892 (x : Prop) : Prop
axiom g893 (x : Prop) : Prop
axiom g894 (x : Prop) : Prop
axiom g895 (x : Prop) : Prop
axiom g896 (x : Prop) : Prop
axiom g897 (x : Prop) : Prop
axiom g898 (x : Prop) : Prop
axiom g899 (x : Prop) : Prop
axiom g900 (x : Prop) : Prop
axiom g901 (x : Prop) : Prop
axiom g902 (x : Prop) : Prop
axiom g903 (x : Prop) : Prop
axiom g904 (x : Prop) : Prop
axiom g905 (x : Prop) : Prop
axiom g906 (x : Prop) : Prop
axiom g907 (x : Prop) : Prop
axiom g908 (x : Prop) : Prop
axiom g909 (x : Prop) : Prop
axiom g910 (x : Prop) : Prop
axiom g911 (x : Prop) : Prop
axiom g912 (x : Prop) : Prop
axiom g913 (x : Prop) : Prop
axiom g914 (x : Prop) : Prop
axiom g915 (x : Prop) : Prop
axiom g916 (x : Prop) : Prop
axiom g917 (x : Prop) : Prop
axiom g918 (x : Prop) : Prop
axiom g919 (x : Prop) : Prop
axiom g920 (x : Prop) : Prop
axiom g921 (x : Prop) : Prop
axiom g922 (x : Prop) : Prop
axiom g923 (x : Prop) : Prop
axiom g924 (x : Prop) : Prop
axiom g925 (x : Prop) : Prop
axiom g926 (x : Prop) : Prop
axiom g927 (x : Prop) : Prop
axiom g928 (x : Prop) : Prop
axiom g929 (x : Prop) : Prop
axiom g930 (x : Prop) : Prop
axiom g931 (x : Prop) : Prop
axiom g932 (x : Prop) : Prop
axiom g933 (x : Prop) : Prop
axiom g934 (x : Prop) : Prop
axiom g935 (x : Prop) : Prop
axiom g936 (x : Prop) : Prop
axiom g937 (x : Prop) : Prop
axiom g938 (x : Prop) : Prop
axiom g939 (x : Prop) : Prop
axiom g940 (x : Prop) : Prop
axiom g941 (x : Prop) : Prop
axiom g942 (x : Prop) : Prop
axiom g943 (x : Prop) : Prop
axiom g944 (x : Prop) : Prop
axiom g945 (x : Prop) : Prop
axiom g946 (x : Prop) : Prop
axiom g947 (x : Prop) : Prop
axiom g948 (x : Prop) : Prop
axiom g949 (x : Prop) : Prop
axiom g950 (x : Prop) : Prop
axiom g951 (x : Prop) : Prop
axiom g952 (x : Prop) : Prop
axiom g953 (x : Prop) : Prop
axiom g954 (x : Prop) : Prop
axiom g955 (x : Prop) : Prop
axiom g956 (x : Prop) : Prop
axiom g957 (x : Prop) : Prop
axiom g958 (x : Prop) : Prop
axiom g959 (x : Prop) : Prop
axiom g960 (x : Prop) : Prop
axiom g961 (x : Prop) : Prop
axiom g962 (x : Prop) : Prop
axiom g963 (x : Prop) : Prop
axiom g964 (x : Prop) : Prop
axiom g965 (x : Prop) : Prop
axiom g966 (x : Prop) : Prop
axiom g967 (x : Prop) : Prop
axiom g968 (x : Prop) : Prop
axiom g969 (x : Prop) : Prop
axiom g970 (x : Prop) : Prop
axiom g971 (x : Prop) : Prop
axiom g972 (x : Prop) : Prop
axiom g973 (x : Prop) : Prop
axiom g974 (x : Prop) : Prop
axiom g975 (x : Prop) : Prop
axiom g976 (x : Prop) : Prop
axiom g977 (x : Prop) : Prop
axiom g978 (x : Prop) : Prop
axiom g979 (x : Prop) : Prop
axiom g980 (x : Prop) : Prop
axiom g981 (x : Prop) : Prop
axiom g982 (x : Prop) : Prop
axiom g983 (x : Prop) : Prop
axiom g984 (x : Prop) : Prop
axiom g985 (x : Prop) : Prop
axiom g986 (x : Prop) : Prop
axiom g987 (x : Prop) : Prop
axiom g988 (x : Prop) : Prop
axiom g989 (x : Prop) : Prop
axiom g990 (x : Prop) : Prop
axiom g991 (x : Prop) : Prop
axiom g992 (x : Prop) : Prop
axiom g993 (x : Prop) : Prop
axiom g994 (x : Prop) : Prop
axiom g995 (x : Prop) : Prop
axiom g996 (x : Prop) : Prop
axiom g997 (x : Prop) : Prop
axiom g998 (x : Prop) : Prop
axiom g999 (x : Prop) : Prop
axiom g1000 (x : Prop) : Prop
axiom g1001 (x : Prop) : Prop
axiom g1002 (x : Prop) : Prop
axiom g1003 (x : Prop) : Prop
axiom g1004 (x : Prop) : Prop
axiom g1005 (x : Prop) : Prop
axiom g1006 (x : Prop) : Prop
axiom g1007 (x : Prop) : Prop
axiom g1008 (x : Prop) : Prop
axiom g1009 (x : Prop) : Prop
axiom g1010 (x : Prop) : Prop
axiom g1011 (x : Prop) : Prop
axiom g1012 (x : Prop) : Prop
axiom g1013 (x : Prop) : Prop
axiom g1014 (x : Prop) : Prop
axiom g1015 (x : Prop) : Prop
axiom g1016 (x : Prop) : Prop
axiom g1017 (x : Prop) : Prop
axiom g1018 (x : Prop) : Prop
axiom g1019 (x : Prop) : Prop
axiom g1020 (x : Prop) : Prop
axiom g1021 (x : Prop) : Prop
axiom g1022 (x : Prop) : Prop
axiom g1023 (x : Prop) : Prop
axiom g1024 (x : Prop) : Prop
axiom g1025 (x : Prop) : Prop
axiom g1026 (x : Prop) : Prop
axiom g1027 (x : Prop) : Prop
axiom g1028 (x : Prop) : Prop
axiom g1029 (x : Prop) : Prop
axiom g1030 (x : Prop) : Prop
axiom g1031 (x : Prop) : Prop
axiom g1032 (x : Prop) : Prop
axiom g1033 (x : Prop) : Prop
axiom g1034 (x : Prop) : Prop
axiom g1035 (x : Prop) : Prop
axiom g1036 (x : Prop) : Prop
axiom g1037 (x : Prop) : Prop
axiom g1038 (x : Prop) : Prop
axiom g1039 (x : Prop) : Prop
axiom g1040 (x : Prop) : Prop
axiom g1041 (x : Prop) : Prop
axiom g1042 (x : Prop) : Prop
axiom g1043 (x : Prop) : Prop
axiom g1044 (x : Prop) : Prop
axiom g1045 (x : Prop) : Prop
axiom g1046 (x : Prop) : Prop
axiom g1047 (x : Prop) : Prop
axiom g1048 (x : Prop) : Prop
axiom g1049 (x : Prop) : Prop
axiom g1050 (x : Prop) : Prop
axiom g1051 (x : Prop) : Prop
axiom g1052 (x : Prop) : Prop
axiom g1053 (x : Prop) : Prop
axiom g1054 (x : Prop) : Prop
axiom g1055 (x : Prop) : Prop
axiom g1056 (x : Prop) : Prop
axiom g1057 (x : Prop) : Prop
axiom g1058 (x : Prop) : Prop
axiom g1059 (x : Prop) : Prop
axiom g1060 (x : Prop) : Prop
axiom g1061 (x : Prop) : Prop
axiom g1062 (x : Prop) : Prop
axiom g1063 (x : Prop) : Prop
axiom g1064 (x : Prop) : Prop
axiom g1065 (x : Prop) : Prop
axiom g1066 (x : Prop) : Prop
axiom g1067 (x : Prop) : Prop
axiom g1068 (x : Prop) : Prop
axiom g1069 (x : Prop) : Prop
axiom g1070 (x : Prop) : Prop
axiom g1071 (x : Prop) : Prop
axiom g1072 (x : Prop) : Prop
axiom g1073 (x : Prop) : Prop
axiom g1074 (x : Prop) : Prop
axiom g1075 (x : Prop) : Prop
axiom g1076 (x : Prop) : Prop
axiom g1077 (x : Prop) : Prop
axiom g1078 (x : Prop) : Prop
axiom g1079 (x : Prop) : Prop
axiom g1080 (x : Prop) : Prop
axiom g1081 (x : Prop) : Prop
axiom g1082 (x : Prop) : Prop
axiom g1083 (x : Prop) : Prop
axiom g1084 (x : Prop) : Prop
axiom g1085 (x : Prop) : Prop
axiom g1086 (x : Prop) : Prop
axiom g1087 (x : Prop) : Prop
axiom g1088 (x : Prop) : Prop
axiom g1089 (x : Prop) : Prop
axiom g1090 (x : Prop) : Prop
axiom g1091 (x : Prop) : Prop
axiom g1092 (x : Prop) : Prop
axiom g1093 (x : Prop) : Prop
axiom g1094 (x : Prop) : Prop
axiom g1095 (x : Prop) : Prop
axiom g1096 (x : Prop) : Prop
axiom g1097 (x : Prop) : Prop
axiom g1098 (x : Prop) : Prop
axiom g1099 (x : Prop) : Prop
axiom g1100 (x : Prop) : Prop
axiom g1101 (x : Prop) : Prop
axiom g1102 (x : Prop) : Prop
axiom g1103 (x : Prop) : Prop
axiom g1104 (x : Prop) : Prop
axiom g1105 (x : Prop) : Prop
axiom g1106 (x : Prop) : Prop
axiom g1107 (x : Prop) : Prop
axiom g1108 (x : Prop) : Prop
axiom g1109 (x : Prop) : Prop
axiom g1110 (x : Prop) : Prop
axiom g1111 (x : Prop) : Prop
axiom g1112 (x : Prop) : Prop
axiom g1113 (x : Prop) : Prop
axiom g1114 (x : Prop) : Prop
axiom g1115 (x : Prop) : Prop
axiom g1116 (x : Prop) : Prop
axiom g1117 (x : Prop) : Prop
axiom g1118 (x : Prop) : Prop
axiom g1119 (x : Prop) : Prop
axiom g1120 (x : Prop) : Prop
axiom g1121 (x : Prop) : Prop
axiom g1122 (x : Prop) : Prop
axiom g1123 (x : Prop) : Prop
axiom g1124 (x : Prop) : Prop
axiom g1125 (x : Prop) : Prop
axiom g1126 (x : Prop) : Prop
axiom g1127 (x : Prop) : Prop
axiom g1128 (x : Prop) : Prop
axiom g1129 (x : Prop) : Prop
axiom g1130 (x : Prop) : Prop
axiom g1131 (x : Prop) : Prop
axiom g1132 (x : Prop) : Prop
axiom g1133 (x : Prop) : Prop
axiom g1134 (x : Prop) : Prop
axiom g1135 (x : Prop) : Prop
axiom g1136 (x : Prop) : Prop
axiom g1137 (x : Prop) : Prop
axiom g1138 (x : Prop) : Prop
axiom g1139 (x : Prop) : Prop
axiom g1140 (x : Prop) : Prop
axiom g1141 (x : Prop) : Prop
axiom g1142 (x : Prop) : Prop
axiom g1143 (x : Prop) : Prop
axiom g1144 (x : Prop) : Prop
axiom g1145 (x : Prop) : Prop
axiom g1146 (x : Prop) : Prop
axiom g1147 (x : Prop) : Prop
axiom g1148 (x : Prop) : Prop
axiom g1149 (x : Prop) : Prop
axiom g1150 (x : Prop) : Prop
axiom g1151 (x : Prop) : Prop
axiom g1152 (x : Prop) : Prop
axiom g1153 (x : Prop) : Prop
axiom g1154 (x : Prop) : Prop
axiom g1155 (x : Prop) : Prop
axiom g1156 (x : Prop) : Prop
axiom g1157 (x : Prop) : Prop
axiom g1158 (x : Prop) : Prop
axiom g1159 (x : Prop) : Prop
axiom g1160 (x : Prop) : Prop
axiom g1161 (x : Prop) : Prop
axiom g1162 (x : Prop) : Prop
axiom g1163 (x : Prop) : Prop
axiom g1164 (x : Prop) : Prop
axiom g1165 (x : Prop) : Prop
axiom g1166 (x : Prop) : Prop
axiom g1167 (x : Prop) : Prop
axiom g1168 (x : Prop) : Prop
axiom g1169 (x : Prop) : Prop
axiom g1170 (x : Prop) : Prop
axiom g1171 (x : Prop) : Prop
axiom g1172 (x : Prop) : Prop
axiom g1173 (x : Prop) : Prop
axiom g1174 (x : Prop) : Prop
axiom g1175 (x : Prop) : Prop
axiom g1176 (x : Prop) : Prop
axiom g1177 (x : Prop) : Prop
axiom g1178 (x : Prop) : Prop
axiom g1179 (x : Prop) : Prop
axiom g1180 (x : Prop) : Prop
axiom g1181 (x : Prop) : Prop
axiom g1182 (x : Prop) : Prop
axiom g1183 (x : Prop) : Prop
axiom g1184 (x : Prop) : Prop
axiom g1185 (x : Prop) : Prop
axiom g1186 (x : Prop) : Prop
axiom g1187 (x : Prop) : Prop
axiom g1188 (x : Prop) : Prop
axiom g1189 (x : Prop) : Prop
axiom g1190 (x : Prop) : Prop
axiom g1191 (x : Prop) : Prop
axiom g1192 (x : Prop) : Prop
axiom g1193 (x : Prop) : Prop
axiom g1194 (x : Prop) : Prop
axiom g1195 (x : Prop) : Prop
axiom g1196 (x : Prop) : Prop
axiom g1197 (x : Prop) : Prop
axiom g1198 (x : Prop) : Prop
axiom g1199 (x : Prop) : Prop
axiom g1200 (x : Prop) : Prop
axiom g1201 (x : Prop) : Prop
axiom g1202 (x : Prop) : Prop
axiom g1203 (x : Prop) : Prop
axiom g1204 (x : Prop) : Prop
axiom g1205 (x : Prop) : Prop
axiom g1206 (x : Prop) : Prop
axiom g1207 (x : Prop) : Prop
axiom g1208 (x : Prop) : Prop
axiom g1209 (x : Prop) : Prop
axiom g1210 (x : Prop) : Prop
axiom g1211 (x : Prop) : Prop
axiom g1212 (x : Prop) : Prop
axiom g1213 (x : Prop) : Prop
axiom g1214 (x : Prop) : Prop
axiom g1215 (x : Prop) : Prop
axiom g1216 (x : Prop) : Prop
axiom g1217 (x : Prop) : Prop
axiom g1218 (x : Prop) : Prop
axiom g1219 (x : Prop) : Prop
axiom g1220 (x : Prop) : Prop
axiom g1221 (x : Prop) : Prop
axiom g1222 (x : Prop) : Prop
axiom g1223 (x : Prop) : Prop
axiom g1224 (x : Prop) : Prop
axiom g1225 (x : Prop) : Prop
axiom g1226 (x : Prop) : Prop
axiom g1227 (x : Prop) : Prop
axiom g1228 (x : Prop) : Prop
axiom g1229 (x : Prop) : Prop
axiom g1230 (x : Prop) : Prop
axiom g1231 (x : Prop) : Prop
axiom g1232 (x : Prop) : Prop
axiom g1233 (x : Prop) : Prop
axiom g1234 (x : Prop) : Prop
axiom g1235 (x : Prop) : Prop
axiom g1236 (x : Prop) : Prop
axiom g1237 (x : Prop) : Prop
axiom g1238 (x : Prop) : Prop
axiom g1239 (x : Prop) : Prop
axiom g1240 (x : Prop) : Prop
axiom g1241 (x : Prop) : Prop
axiom g1242 (x : Prop) : Prop
axiom g1243 (x : Prop) : Prop
axiom g1244 (x : Prop) : Prop
axiom g1245 (x : Prop) : Prop
axiom g1246 (x : Prop) : Prop
axiom g1247 (x : Prop) : Prop
axiom g1248 (x : Prop) : Prop
axiom g1249 (x : Prop) : Prop
axiom g1250 (x : Prop) : Prop
axiom g1251 (x : Prop) : Prop
axiom g1252 (x : Prop) : Prop
axiom g1253 (x : Prop) : Prop
axiom g1254 (x : Prop) : Prop
axiom g1255 (x : Prop) : Prop
axiom g1256 (x : Prop) : Prop
axiom g1257 (x : Prop) : Prop
axiom g1258 (x : Prop) : Prop
axiom g1259 (x : Prop) : Prop
axiom g1260 (x : Prop) : Prop
axiom g1261 (x : Prop) : Prop
axiom g1262 (x : Prop) : Prop
axiom g1263 (x : Prop) : Prop
axiom g1264 (x : Prop) : Prop
axiom g1265 (x : Prop) : Prop
axiom g1266 (x : Prop) : Prop
axiom g1267 (x : Prop) : Prop
axiom g1268 (x : Prop) : Prop
axiom g1269 (x : Prop) : Prop
axiom g1270 (x : Prop) : Prop
axiom g1271 (x : Prop) : Prop
axiom g1272 (x : Prop) : Prop
axiom g1273 (x : Prop) : Prop
axiom g1274 (x : Prop) : Prop
axiom g1275 (x : Prop) : Prop
axiom g1276 (x : Prop) : Prop
axiom g1277 (x : Prop) : Prop
axiom g1278 (x : Prop) : Prop
axiom g1279 (x : Prop) : Prop
axiom g1280 (x : Prop) : Prop
axiom g1281 (x : Prop) : Prop
axiom g1282 (x : Prop) : Prop
axiom g1283 (x : Prop) : Prop
axiom g1284 (x : Prop) : Prop
axiom g1285 (x : Prop) : Prop
axiom g1286 (x : Prop) : Prop
axiom g1287 (x : Prop) : Prop
axiom g1288 (x : Prop) : Prop
axiom g1289 (x : Prop) : Prop
axiom g1290 (x : Prop) : Prop
axiom g1291 (x : Prop) : Prop
axiom g1292 (x : Prop) : Prop
axiom g1293 (x : Prop) : Prop
axiom g1294 (x : Prop) : Prop
axiom g1295 (x : Prop) : Prop
axiom g1296 (x : Prop) : Prop
axiom g1297 (x : Prop) : Prop
axiom g1298 (x : Prop) : Prop
axiom g1299 (x : Prop) : Prop
axiom g1300 (x : Prop) : Prop
axiom g1301 (x : Prop) : Prop
axiom g1302 (x : Prop) : Prop
axiom g1303 (x : Prop) : Prop
axiom g1304 (x : Prop) : Prop
axiom g1305 (x : Prop) : Prop
axiom g1306 (x : Prop) : Prop
axiom g1307 (x : Prop) : Prop
axiom g1308 (x : Prop) : Prop
axiom g1309 (x : Prop) : Prop
axiom g1310 (x : Prop) : Prop
axiom g1311 (x : Prop) : Prop
axiom g1312 (x : Prop) : Prop
axiom g1313 (x : Prop) : Prop
axiom g1314 (x : Prop) : Prop
axiom g1315 (x : Prop) : Prop
axiom g1316 (x : Prop) : Prop
axiom g1317 (x : Prop) : Prop
axiom g1318 (x : Prop) : Prop
axiom g1319 (x : Prop) : Prop
axiom g1320 (x : Prop) : Prop
axiom g1321 (x : Prop) : Prop
axiom g1322 (x : Prop) : Prop
axiom g1323 (x : Prop) : Prop
axiom g1324 (x : Prop) : Prop
axiom g1325 (x : Prop) : Prop
axiom g1326 (x : Prop) : Prop
axiom g1327 (x : Prop) : Prop
axiom g1328 (x : Prop) : Prop
axiom g1329 (x : Prop) : Prop
axiom g1330 (x : Prop) : Prop
axiom g1331 (x : Prop) : Prop
axiom g1332 (x : Prop) : Prop
axiom g1333 (x : Prop) : Prop
axiom g1334 (x : Prop) : Prop
axiom g1335 (x : Prop) : Prop
axiom g1336 (x : Prop) : Prop
axiom g1337 (x : Prop) : Prop
axiom g1338 (x : Prop) : Prop
axiom g1339 (x : Prop) : Prop
axiom g1340 (x : Prop) : Prop
axiom g1341 (x : Prop) : Prop
axiom g1342 (x : Prop) : Prop
axiom g1343 (x : Prop) : Prop
axiom g1344 (x : Prop) : Prop
axiom g1345 (x : Prop) : Prop
axiom g1346 (x : Prop) : Prop
axiom g1347 (x : Prop) : Prop
axiom g1348 (x : Prop) : Prop
axiom g1349 (x : Prop) : Prop
axiom g1350 (x : Prop) : Prop
axiom g1351 (x : Prop) : Prop
axiom g1352 (x : Prop) : Prop
axiom g1353 (x : Prop) : Prop
axiom g1354 (x : Prop) : Prop
axiom g1355 (x : Prop) : Prop
axiom g1356 (x : Prop) : Prop
axiom g1357 (x : Prop) : Prop
axiom g1358 (x : Prop) : Prop
axiom g1359 (x : Prop) : Prop
axiom g1360 (x : Prop) : Prop
axiom g1361 (x : Prop) : Prop
axiom g1362 (x : Prop) : Prop
axiom g1363 (x : Prop) : Prop
axiom g1364 (x : Prop) : Prop
axiom g1365 (x : Prop) : Prop
axiom g1366 (x : Prop) : Prop
axiom g1367 (x : Prop) : Prop
axiom g1368 (x : Prop) : Prop
axiom g1369 (x : Prop) : Prop
axiom g1370 (x : Prop) : Prop
axiom g1371 (x : Prop) : Prop
axiom g1372 (x : Prop) : Prop
axiom g1373 (x : Prop) : Prop
axiom g1374 (x : Prop) : Prop
axiom g1375 (x : Prop) : Prop
axiom g1376 (x : Prop) : Prop
axiom g1377 (x : Prop) : Prop
axiom g1378 (x : Prop) : Prop
axiom g1379 (x : Prop) : Prop
axiom g1380 (x : Prop) : Prop
axiom g1381 (x : Prop) : Prop
axiom g1382 (x : Prop) : Prop
axiom g1383 (x : Prop) : Prop
axiom g1384 (x : Prop) : Prop
axiom g1385 (x : Prop) : Prop
axiom g1386 (x : Prop) : Prop
axiom g1387 (x : Prop) : Prop
axiom g1388 (x : Prop) : Prop
axiom g1389 (x : Prop) : Prop
axiom g1390 (x : Prop) : Prop
axiom g1391 (x : Prop) : Prop
axiom g1392 (x : Prop) : Prop
axiom g1393 (x : Prop) : Prop
axiom g1394 (x : Prop) : Prop
axiom g1395 (x : Prop) : Prop
axiom g1396 (x : Prop) : Prop
axiom g1397 (x : Prop) : Prop
axiom g1398 (x : Prop) : Prop
axiom g1399 (x : Prop) : Prop
axiom g1400 (x : Prop) : Prop
axiom g1401 (x : Prop) : Prop
axiom g1402 (x : Prop) : Prop
axiom g1403 (x : Prop) : Prop
axiom g1404 (x : Prop) : Prop
axiom g1405 (x : Prop) : Prop
axiom g1406 (x : Prop) : Prop
axiom g1407 (x : Prop) : Prop
axiom g1408 (x : Prop) : Prop
axiom g1409 (x : Prop) : Prop
axiom g1410 (x : Prop) : Prop
axiom g1411 (x : Prop) : Prop
axiom g1412 (x : Prop) : Prop
axiom g1413 (x : Prop) : Prop
axiom g1414 (x : Prop) : Prop
axiom g1415 (x : Prop) : Prop
axiom g1416 (x : Prop) : Prop
axiom g1417 (x : Prop) : Prop
axiom g1418 (x : Prop) : Prop
axiom g1419 (x : Prop) : Prop
axiom g1420 (x : Prop) : Prop
axiom g1421 (x : Prop) : Prop
axiom g1422 (x : Prop) : Prop
axiom g1423 (x : Prop) : Prop
axiom g1424 (x : Prop) : Prop
axiom g1425 (x : Prop) : Prop
axiom g1426 (x : Prop) : Prop
axiom g1427 (x : Prop) : Prop
axiom g1428 (x : Prop) : Prop
axiom g1429 (x : Prop) : Prop
axiom g1430 (x : Prop) : Prop
axiom g1431 (x : Prop) : Prop
axiom g1432 (x : Prop) : Prop
axiom g1433 (x : Prop) : Prop
axiom g1434 (x : Prop) : Prop
axiom g1435 (x : Prop) : Prop
axiom g1436 (x : Prop) : Prop
axiom g1437 (x : Prop) : Prop
axiom g1438 (x : Prop) : Prop
axiom g1439 (x : Prop) : Prop
axiom g1440 (x : Prop) : Prop
axiom g1441 (x : Prop) : Prop
axiom g1442 (x : Prop) : Prop
axiom g1443 (x : Prop) : Prop
axiom g1444 (x : Prop) : Prop
axiom g1445 (x : Prop) : Prop
axiom g1446 (x : Prop) : Prop
axiom g1447 (x : Prop) : Prop
axiom g1448 (x : Prop) : Prop
axiom g1449 (x : Prop) : Prop
axiom g1450 (x : Prop) : Prop
axiom g1451 (x : Prop) : Prop
axiom g1452 (x : Prop) : Prop
axiom g1453 (x : Prop) : Prop
axiom g1454 (x : Prop) : Prop
axiom g1455 (x : Prop) : Prop
axiom g1456 (x : Prop) : Prop
axiom g1457 (x : Prop) : Prop
axiom g1458 (x : Prop) : Prop
axiom g1459 (x : Prop) : Prop
axiom g1460 (x : Prop) : Prop
axiom g1461 (x : Prop) : Prop
axiom g1462 (x : Prop) : Prop
axiom g1463 (x : Prop) : Prop
axiom g1464 (x : Prop) : Prop
axiom g1465 (x : Prop) : Prop
axiom g1466 (x : Prop) : Prop
axiom g1467 (x : Prop) : Prop
axiom g1468 (x : Prop) : Prop
axiom g1469 (x : Prop) : Prop
axiom g1470 (x : Prop) : Prop
axiom g1471 (x : Prop) : Prop
axiom g1472 (x : Prop) : Prop
axiom g1473 (x : Prop) : Prop
axiom g1474 (x : Prop) : Prop
axiom g1475 (x : Prop) : Prop
axiom g1476 (x : Prop) : Prop
axiom g1477 (x : Prop) : Prop
axiom g1478 (x : Prop) : Prop
axiom g1479 (x : Prop) : Prop
axiom g1480 (x : Prop) : Prop
axiom g1481 (x : Prop) : Prop
axiom g1482 (x : Prop) : Prop
axiom g1483 (x : Prop) : Prop
axiom g1484 (x : Prop) : Prop
axiom g1485 (x : Prop) : Prop
axiom g1486 (x : Prop) : Prop
axiom g1487 (x : Prop) : Prop
axiom g1488 (x : Prop) : Prop
axiom g1489 (x : Prop) : Prop
axiom g1490 (x : Prop) : Prop
axiom g1491 (x : Prop) : Prop
axiom g1492 (x : Prop) : Prop
axiom g1493 (x : Prop) : Prop
axiom g1494 (x : Prop) : Prop
axiom g1495 (x : Prop) : Prop
axiom g1496 (x : Prop) : Prop
axiom g1497 (x : Prop) : Prop
axiom g1498 (x : Prop) : Prop
axiom g1499 (x : Prop) : Prop
axiom g1500 (x : Prop) : Prop
axiom g1501 (x : Prop) : Prop
axiom g1502 (x : Prop) : Prop
axiom g1503 (x : Prop) : Prop
axiom g1504 (x : Prop) : Prop
axiom g1505 (x : Prop) : Prop
axiom g1506 (x : Prop) : Prop
axiom g1507 (x : Prop) : Prop
axiom g1508 (x : Prop) : Prop
axiom g1509 (x : Prop) : Prop
axiom g1510 (x : Prop) : Prop
axiom g1511 (x : Prop) : Prop
axiom g1512 (x : Prop) : Prop
axiom g1513 (x : Prop) : Prop
axiom g1514 (x : Prop) : Prop
axiom g1515 (x : Prop) : Prop
axiom g1516 (x : Prop) : Prop
axiom g1517 (x : Prop) : Prop
axiom g1518 (x : Prop) : Prop
axiom g1519 (x : Prop) : Prop
axiom g1520 (x : Prop) : Prop
axiom g1521 (x : Prop) : Prop
axiom g1522 (x : Prop) : Prop
axiom g1523 (x : Prop) : Prop
axiom g1524 (x : Prop) : Prop
axiom g1525 (x : Prop) : Prop
axiom g1526 (x : Prop) : Prop
axiom g1527 (x : Prop) : Prop
axiom g1528 (x : Prop) : Prop
axiom g1529 (x : Prop) : Prop
axiom g1530 (x : Prop) : Prop
axiom g1531 (x : Prop) : Prop
axiom g1532 (x : Prop) : Prop
axiom g1533 (x : Prop) : Prop
axiom g1534 (x : Prop) : Prop
axiom g1535 (x : Prop) : Prop
axiom g1536 (x : Prop) : Prop
axiom g1537 (x : Prop) : Prop
axiom g1538 (x : Prop) : Prop
axiom g1539 (x : Prop) : Prop
axiom g1540 (x : Prop) : Prop
axiom g1541 (x : Prop) : Prop
axiom g1542 (x : Prop) : Prop
axiom g1543 (x : Prop) : Prop
axiom g1544 (x : Prop) : Prop
axiom g1545 (x : Prop) : Prop
axiom g1546 (x : Prop) : Prop
axiom g1547 (x : Prop) : Prop
axiom g1548 (x : Prop) : Prop
axiom g1549 (x : Prop) : Prop
axiom g1550 (x : Prop) : Prop
axiom g1551 (x : Prop) : Prop
axiom g1552 (x : Prop) : Prop
axiom g1553 (x : Prop) : Prop
axiom g1554 (x : Prop) : Prop
axiom g1555 (x : Prop) : Prop
axiom g1556 (x : Prop) : Prop
axiom g1557 (x : Prop) : Prop
axiom g1558 (x : Prop) : Prop
axiom g1559 (x : Prop) : Prop
axiom g1560 (x : Prop) : Prop
axiom g1561 (x : Prop) : Prop
axiom g1562 (x : Prop) : Prop
axiom g1563 (x : Prop) : Prop
axiom g1564 (x : Prop) : Prop
axiom g1565 (x : Prop) : Prop
axiom g1566 (x : Prop) : Prop
axiom g1567 (x : Prop) : Prop
axiom g1568 (x : Prop) : Prop
axiom g1569 (x : Prop) : Prop
axiom g1570 (x : Prop) : Prop
axiom g1571 (x : Prop) : Prop
axiom g1572 (x : Prop) : Prop
axiom g1573 (x : Prop) : Prop
axiom g1574 (x : Prop) : Prop
axiom g1575 (x : Prop) : Prop
axiom g1576 (x : Prop) : Prop
axiom g1577 (x : Prop) : Prop
axiom g1578 (x : Prop) : Prop
axiom g1579 (x : Prop) : Prop
axiom g1580 (x : Prop) : Prop
axiom g1581 (x : Prop) : Prop
axiom g1582 (x : Prop) : Prop
axiom g1583 (x : Prop) : Prop
axiom g1584 (x : Prop) : Prop
axiom g1585 (x : Prop) : Prop
axiom g1586 (x : Prop) : Prop
axiom g1587 (x : Prop) : Prop
axiom g1588 (x : Prop) : Prop
axiom g1589 (x : Prop) : Prop
axiom g1590 (x : Prop) : Prop
axiom g1591 (x : Prop) : Prop
axiom g1592 (x : Prop) : Prop
axiom g1593 (x : Prop) : Prop
axiom g1594 (x : Prop) : Prop
axiom g1595 (x : Prop) : Prop
axiom g1596 (x : Prop) : Prop
axiom g1597 (x : Prop) : Prop
axiom g1598 (x : Prop) : Prop
axiom g1599 (x : Prop) : Prop
axiom g1600 (x : Prop) : Prop
axiom g1601 (x : Prop) : Prop
axiom g1602 (x : Prop) : Prop
axiom g1603 (x : Prop) : Prop
axiom g1604 (x : Prop) : Prop
axiom g1605 (x : Prop) : Prop
axiom g1606 (x : Prop) : Prop
axiom g1607 (x : Prop) : Prop
axiom g1608 (x : Prop) : Prop
axiom g1609 (x : Prop) : Prop
axiom g1610 (x : Prop) : Prop
axiom g1611 (x : Prop) : Prop
axiom g1612 (x : Prop) : Prop
axiom g1613 (x : Prop) : Prop
axiom g1614 (x : Prop) : Prop
axiom g1615 (x : Prop) : Prop
axiom g1616 (x : Prop) : Prop
axiom g1617 (x : Prop) : Prop
axiom g1618 (x : Prop) : Prop
axiom g1619 (x : Prop) : Prop
axiom g1620 (x : Prop) : Prop
axiom g1621 (x : Prop) : Prop
axiom g1622 (x : Prop) : Prop
axiom g1623 (x : Prop) : Prop
axiom g1624 (x : Prop) : Prop
axiom g1625 (x : Prop) : Prop
axiom g1626 (x : Prop) : Prop
axiom g1627 (x : Prop) : Prop
axiom g1628 (x : Prop) : Prop
axiom g1629 (x : Prop) : Prop
axiom g1630 (x : Prop) : Prop
axiom g1631 (x : Prop) : Prop
axiom g1632 (x : Prop) : Prop
axiom g1633 (x : Prop) : Prop
axiom g1634 (x : Prop) : Prop
axiom g1635 (x : Prop) : Prop
axiom g1636 (x : Prop) : Prop
axiom g1637 (x : Prop) : Prop
axiom g1638 (x : Prop) : Prop
axiom g1639 (x : Prop) : Prop
axiom g1640 (x : Prop) : Prop
axiom g1641 (x : Prop) : Prop
axiom g1642 (x : Prop) : Prop
axiom g1643 (x : Prop) : Prop
axiom g1644 (x : Prop) : Prop
axiom g1645 (x : Prop) : Prop
axiom g1646 (x : Prop) : Prop
axiom g1647 (x : Prop) : Prop
axiom g1648 (x : Prop) : Prop
axiom g1649 (x : Prop) : Prop
axiom g1650 (x : Prop) : Prop
axiom g1651 (x : Prop) : Prop
axiom g1652 (x : Prop) : Prop
axiom g1653 (x : Prop) : Prop
axiom g1654 (x : Prop) : Prop
axiom g1655 (x : Prop) : Prop
axiom g1656 (x : Prop) : Prop
axiom g1657 (x : Prop) : Prop
axiom g1658 (x : Prop) : Prop
axiom g1659 (x : Prop) : Prop
axiom g1660 (x : Prop) : Prop
axiom g1661 (x : Prop) : Prop
axiom g1662 (x : Prop) : Prop
axiom g1663 (x : Prop) : Prop
axiom g1664 (x : Prop) : Prop
axiom g1665 (x : Prop) : Prop
axiom g1666 (x : Prop) : Prop
axiom g1667 (x : Prop) : Prop
axiom g1668 (x : Prop) : Prop
axiom g1669 (x : Prop) : Prop
axiom g1670 (x : Prop) : Prop
axiom g1671 (x : Prop) : Prop
axiom g1672 (x : Prop) : Prop
axiom g1673 (x : Prop) : Prop
axiom g1674 (x : Prop) : Prop
axiom g1675 (x : Prop) : Prop
axiom g1676 (x : Prop) : Prop
axiom g1677 (x : Prop) : Prop
axiom g1678 (x : Prop) : Prop
axiom g1679 (x : Prop) : Prop
axiom g1680 (x : Prop) : Prop
axiom g1681 (x : Prop) : Prop
axiom g1682 (x : Prop) : Prop
axiom g1683 (x : Prop) : Prop
axiom g1684 (x : Prop) : Prop
axiom g1685 (x : Prop) : Prop
axiom g1686 (x : Prop) : Prop
axiom g1687 (x : Prop) : Prop
axiom g1688 (x : Prop) : Prop
axiom g1689 (x : Prop) : Prop
axiom g1690 (x : Prop) : Prop
axiom g1691 (x : Prop) : Prop
axiom g1692 (x : Prop) : Prop
axiom g1693 (x : Prop) : Prop
axiom g1694 (x : Prop) : Prop
axiom g1695 (x : Prop) : Prop
axiom g1696 (x : Prop) : Prop
axiom g1697 (x : Prop) : Prop
axiom g1698 (x : Prop) : Prop
axiom g1699 (x : Prop) : Prop
axiom g1700 (x : Prop) : Prop
axiom g1701 (x : Prop) : Prop
axiom g1702 (x : Prop) : Prop
axiom g1703 (x : Prop) : Prop
axiom g1704 (x : Prop) : Prop
axiom g1705 (x : Prop) : Prop
axiom g1706 (x : Prop) : Prop
axiom g1707 (x : Prop) : Prop
axiom g1708 (x : Prop) : Prop
axiom g1709 (x : Prop) : Prop
axiom g1710 (x : Prop) : Prop
axiom g1711 (x : Prop) : Prop
axiom g1712 (x : Prop) : Prop
axiom g1713 (x : Prop) : Prop
axiom g1714 (x : Prop) : Prop
axiom g1715 (x : Prop) : Prop
axiom g1716 (x : Prop) : Prop
axiom g1717 (x : Prop) : Prop
axiom g1718 (x : Prop) : Prop
axiom g1719 (x : Prop) : Prop
axiom g1720 (x : Prop) : Prop
axiom g1721 (x : Prop) : Prop
axiom g1722 (x : Prop) : Prop
axiom g1723 (x : Prop) : Prop
axiom g1724 (x : Prop) : Prop
axiom g1725 (x : Prop) : Prop
axiom g1726 (x : Prop) : Prop
axiom g1727 (x : Prop) : Prop
axiom g1728 (x : Prop) : Prop
axiom g1729 (x : Prop) : Prop
axiom g1730 (x : Prop) : Prop
axiom g1731 (x : Prop) : Prop
axiom g1732 (x : Prop) : Prop
axiom g1733 (x : Prop) : Prop
axiom g1734 (x : Prop) : Prop
axiom g1735 (x : Prop) : Prop
axiom g1736 (x : Prop) : Prop
axiom g1737 (x : Prop) : Prop
axiom g1738 (x : Prop) : Prop
axiom g1739 (x : Prop) : Prop
axiom g1740 (x : Prop) : Prop
axiom g1741 (x : Prop) : Prop
axiom g1742 (x : Prop) : Prop
axiom g1743 (x : Prop) : Prop
axiom g1744 (x : Prop) : Prop
axiom g1745 (x : Prop) : Prop
axiom g1746 (x : Prop) : Prop
axiom g1747 (x : Prop) : Prop
axiom g1748 (x : Prop) : Prop
axiom g1749 (x : Prop) : Prop
axiom g1750 (x : Prop) : Prop
axiom g1751 (x : Prop) : Prop
axiom g1752 (x : Prop) : Prop
axiom g1753 (x : Prop) : Prop
axiom g1754 (x : Prop) : Prop
axiom g1755 (x : Prop) : Prop
axiom g1756 (x : Prop) : Prop
axiom g1757 (x : Prop) : Prop
axiom g1758 (x : Prop) : Prop
axiom g1759 (x : Prop) : Prop
axiom g1760 (x : Prop) : Prop
axiom g1761 (x : Prop) : Prop
axiom g1762 (x : Prop) : Prop
axiom g1763 (x : Prop) : Prop
axiom g1764 (x : Prop) : Prop
axiom g1765 (x : Prop) : Prop
axiom g1766 (x : Prop) : Prop
axiom g1767 (x : Prop) : Prop
axiom g1768 (x : Prop) : Prop
axiom g1769 (x : Prop) : Prop
axiom g1770 (x : Prop) : Prop
axiom g1771 (x : Prop) : Prop
axiom g1772 (x : Prop) : Prop
axiom g1773 (x : Prop) : Prop
axiom g1774 (x : Prop) : Prop
axiom g1775 (x : Prop) : Prop
axiom g1776 (x : Prop) : Prop
axiom g1777 (x : Prop) : Prop
axiom g1778 (x : Prop) : Prop
axiom g1779 (x : Prop) : Prop
axiom g1780 (x : Prop) : Prop
axiom g1781 (x : Prop) : Prop
axiom g1782 (x : Prop) : Prop
axiom g1783 (x : Prop) : Prop
axiom g1784 (x : Prop) : Prop
axiom g1785 (x : Prop) : Prop
axiom g1786 (x : Prop) : Prop
axiom g1787 (x : Prop) : Prop
axiom g1788 (x : Prop) : Prop
axiom g1789 (x : Prop) : Prop
axiom g1790 (x : Prop) : Prop
axiom g1791 (x : Prop) : Prop
axiom g1792 (x : Prop) : Prop
axiom g1793 (x : Prop) : Prop
axiom g1794 (x : Prop) : Prop
axiom g1795 (x : Prop) : Prop
axiom g1796 (x : Prop) : Prop
axiom g1797 (x : Prop) : Prop
axiom g1798 (x : Prop) : Prop
axiom g1799 (x : Prop) : Prop
axiom g1800 (x : Prop) : Prop
axiom g1801 (x : Prop) : Prop
axiom g1802 (x : Prop) : Prop
axiom g1803 (x : Prop) : Prop
axiom g1804 (x : Prop) : Prop
axiom g1805 (x : Prop) : Prop
axiom g1806 (x : Prop) : Prop
axiom g1807 (x : Prop) : Prop
axiom g1808 (x : Prop) : Prop
axiom g1809 (x : Prop) : Prop
axiom g1810 (x : Prop) : Prop
axiom g1811 (x : Prop) : Prop
axiom g1812 (x : Prop) : Prop
axiom g1813 (x : Prop) : Prop
axiom g1814 (x : Prop) : Prop
axiom g1815 (x : Prop) : Prop
axiom g1816 (x : Prop) : Prop
axiom g1817 (x : Prop) : Prop
axiom g1818 (x : Prop) : Prop
axiom g1819 (x : Prop) : Prop
axiom g1820 (x : Prop) : Prop
axiom g1821 (x : Prop) : Prop
axiom g1822 (x : Prop) : Prop
axiom g1823 (x : Prop) : Prop
axiom g1824 (x : Prop) : Prop
axiom g1825 (x : Prop) : Prop
axiom g1826 (x : Prop) : Prop
axiom g1827 (x : Prop) : Prop
axiom g1828 (x : Prop) : Prop
axiom g1829 (x : Prop) : Prop
axiom g1830 (x : Prop) : Prop
axiom g1831 (x : Prop) : Prop
axiom g1832 (x : Prop) : Prop
axiom g1833 (x : Prop) : Prop
axiom g1834 (x : Prop) : Prop
axiom g1835 (x : Prop) : Prop
axiom g1836 (x : Prop) : Prop
axiom g1837 (x : Prop) : Prop
axiom g1838 (x : Prop) : Prop
axiom g1839 (x : Prop) : Prop
axiom g1840 (x : Prop) : Prop
axiom g1841 (x : Prop) : Prop
axiom g1842 (x : Prop) : Prop
axiom g1843 (x : Prop) : Prop
axiom g1844 (x : Prop) : Prop
axiom g1845 (x : Prop) : Prop
axiom g1846 (x : Prop) : Prop
axiom g1847 (x : Prop) : Prop
axiom g1848 (x : Prop) : Prop
axiom g1849 (x : Prop) : Prop
axiom g1850 (x : Prop) : Prop
axiom g1851 (x : Prop) : Prop
axiom g1852 (x : Prop) : Prop
axiom g1853 (x : Prop) : Prop
axiom g1854 (x : Prop) : Prop
axiom g1855 (x : Prop) : Prop
axiom g1856 (x : Prop) : Prop
axiom g1857 (x : Prop) : Prop
axiom g1858 (x : Prop) : Prop
axiom g1859 (x : Prop) : Prop
axiom g1860 (x : Prop) : Prop
axiom g1861 (x : Prop) : Prop
axiom g1862 (x : Prop) : Prop
axiom g1863 (x : Prop) : Prop
axiom g1864 (x : Prop) : Prop
axiom g1865 (x : Prop) : Prop
axiom g1866 (x : Prop) : Prop
axiom g1867 (x : Prop) : Prop
axiom g1868 (x : Prop) : Prop
axiom g1869 (x : Prop) : Prop
axiom g1870 (x : Prop) : Prop
axiom g1871 (x : Prop) : Prop
axiom g1872 (x : Prop) : Prop
axiom g1873 (x : Prop) : Prop
axiom g1874 (x : Prop) : Prop
axiom g1875 (x : Prop) : Prop
axiom g1876 (x : Prop) : Prop
axiom g1877 (x : Prop) : Prop
axiom g1878 (x : Prop) : Prop
axiom g1879 (x : Prop) : Prop
axiom g1880 (x : Prop) : Prop
axiom g1881 (x : Prop) : Prop
axiom g1882 (x : Prop) : Prop
axiom g1883 (x : Prop) : Prop
axiom g1884 (x : Prop) : Prop
axiom g1885 (x : Prop) : Prop
axiom g1886 (x : Prop) : Prop
axiom g1887 (x : Prop) : Prop
axiom g1888 (x : Prop) : Prop
axiom g1889 (x : Prop) : Prop
axiom g1890 (x : Prop) : Prop
axiom g1891 (x : Prop) : Prop
axiom g1892 (x : Prop) : Prop
axiom g1893 (x : Prop) : Prop
axiom g1894 (x : Prop) : Prop
axiom g1895 (x : Prop) : Prop
axiom g1896 (x : Prop) : Prop
axiom g1897 (x : Prop) : Prop
axiom g1898 (x : Prop) : Prop
axiom g1899 (x : Prop) : Prop
axiom g1900 (x : Prop) : Prop
axiom g1901 (x : Prop) : Prop
axiom g1902 (x : Prop) : Prop
axiom g1903 (x : Prop) : Prop
axiom g1904 (x : Prop) : Prop
axiom g1905 (x : Prop) : Prop
axiom g1906 (x : Prop) : Prop
axiom g1907 (x : Prop) : Prop
axiom g1908 (x : Prop) : Prop
axiom g1909 (x : Prop) : Prop
axiom g1910 (x : Prop) : Prop
axiom g1911 (x : Prop) : Prop
axiom g1912 (x : Prop) : Prop
axiom g1913 (x : Prop) : Prop
axiom g1914 (x : Prop) : Prop
axiom g1915 (x : Prop) : Prop
axiom g1916 (x : Prop) : Prop
axiom g1917 (x : Prop) : Prop
axiom g1918 (x : Prop) : Prop
axiom g1919 (x : Prop) : Prop
axiom g1920 (x : Prop) : Prop
axiom g1921 (x : Prop) : Prop
axiom g1922 (x : Prop) : Prop
axiom g1923 (x : Prop) : Prop
axiom g1924 (x : Prop) : Prop
axiom g1925 (x : Prop) : Prop
axiom g1926 (x : Prop) : Prop
axiom g1927 (x : Prop) : Prop
axiom g1928 (x : Prop) : Prop
axiom g1929 (x : Prop) : Prop
axiom g1930 (x : Prop) : Prop
axiom g1931 (x : Prop) : Prop
axiom g1932 (x : Prop) : Prop
axiom g1933 (x : Prop) : Prop
axiom g1934 (x : Prop) : Prop
axiom g1935 (x : Prop) : Prop
axiom g1936 (x : Prop) : Prop
axiom g1937 (x : Prop) : Prop
axiom g1938 (x : Prop) : Prop
axiom g1939 (x : Prop) : Prop
axiom g1940 (x : Prop) : Prop
axiom g1941 (x : Prop) : Prop
axiom g1942 (x : Prop) : Prop
axiom g1943 (x : Prop) : Prop
axiom g1944 (x : Prop) : Prop
axiom g1945 (x : Prop) : Prop
axiom g1946 (x : Prop) : Prop
axiom g1947 (x : Prop) : Prop
axiom g1948 (x : Prop) : Prop
axiom g1949 (x : Prop) : Prop
axiom g1950 (x : Prop) : Prop
axiom g1951 (x : Prop) : Prop
axiom g1952 (x : Prop) : Prop
axiom g1953 (x : Prop) : Prop
axiom g1954 (x : Prop) : Prop
axiom g1955 (x : Prop) : Prop
axiom g1956 (x : Prop) : Prop
axiom g1957 (x : Prop) : Prop
axiom g1958 (x : Prop) : Prop
axiom g1959 (x : Prop) : Prop
axiom g1960 (x : Prop) : Prop
axiom g1961 (x : Prop) : Prop
axiom g1962 (x : Prop) : Prop
axiom g1963 (x : Prop) : Prop
axiom g1964 (x : Prop) : Prop
axiom g1965 (x : Prop) : Prop
axiom g1966 (x : Prop) : Prop
axiom g1967 (x : Prop) : Prop
axiom g1968 (x : Prop) : Prop
axiom g1969 (x : Prop) : Prop
axiom g1970 (x : Prop) : Prop
axiom g1971 (x : Prop) : Prop
axiom g1972 (x : Prop) : Prop
axiom g1973 (x : Prop) : Prop
axiom g1974 (x : Prop) : Prop
axiom g1975 (x : Prop) : Prop
axiom g1976 (x : Prop) : Prop
axiom g1977 (x : Prop) : Prop
axiom g1978 (x : Prop) : Prop
axiom g1979 (x : Prop) : Prop
axiom g1980 (x : Prop) : Prop
axiom g1981 (x : Prop) : Prop
axiom g1982 (x : Prop) : Prop
axiom g1983 (x : Prop) : Prop
axiom g1984 (x : Prop) : Prop
axiom g1985 (x : Prop) : Prop
axiom g1986 (x : Prop) : Prop
axiom g1987 (x : Prop) : Prop
axiom g1988 (x : Prop) : Prop
axiom g1989 (x : Prop) : Prop
axiom g1990 (x : Prop) : Prop
axiom g1991 (x : Prop) : Prop
axiom g1992 (x : Prop) : Prop
axiom g1993 (x : Prop) : Prop
axiom g1994 (x : Prop) : Prop
axiom g1995 (x : Prop) : Prop
axiom g1996 (x : Prop) : Prop
axiom g1997 (x : Prop) : Prop
axiom g1998 (x : Prop) : Prop
axiom g1999 (x : Prop) : Prop
@[simp] axiom s0 (x : Prop) : f (g1 x) = f (g0 x)
@[simp] axiom s1 (x : Prop) : f (g2 x) = f (g1 x)
@[simp] axiom s2 (x : Prop) : f (g3 x) = f (g2 x)
@[simp] axiom s3 (x : Prop) : f (g4 x) = f (g3 x)
@[simp] axiom s4 (x : Prop) : f (g5 x) = f (g4 x)
@[simp] axiom s5 (x : Prop) : f (g6 x) = f (g5 x)
@[simp] axiom s6 (x : Prop) : f (g7 x) = f (g6 x)
@[simp] axiom s7 (x : Prop) : f (g8 x) = f (g7 x)
@[simp] axiom s8 (x : Prop) : f (g9 x) = f (g8 x)
@[simp] axiom s9 (x : Prop) : f (g10 x) = f (g9 x)
@[simp] axiom s10 (x : Prop) : f (g11 x) = f (g10 x)
@[simp] axiom s11 (x : Prop) : f (g12 x) = f (g11 x)
@[simp] axiom s12 (x : Prop) : f (g13 x) = f (g12 x)
@[simp] axiom s13 (x : Prop) : f (g14 x) = f (g13 x)
@[simp] axiom s14 (x : Prop) : f (g15 x) = f (g14 x)
@[simp] axiom s15 (x : Prop) : f (g16 x) = f (g15 x)
@[simp] axiom s16 (x : Prop) : f (g17 x) = f (g16 x)
@[simp] axiom s17 (x : Prop) : f (g18 x) = f (g17 x)
@[simp] axiom s18 (x : Prop) : f (g19 x) = f (g18 x)
@[simp] axiom s19 (x : Prop) : f (g20 x) = f (g19 x)
@[simp] axiom s20 (x : Prop) : f (g21 x) = f (g20 x)
@[simp] axiom s21 (x : Prop) : f (g22 x) = f (g21 x)
@[simp] axiom s22 (x : Prop) : f (g23 x) = f (g22 x)
@[simp] axiom s23 (x : Prop) : f (g24 x) = f (g23 x)
@[simp] axiom s24 (x : Prop) : f (g25 x) = f (g24 x)
@[simp] axiom s25 (x : Prop) : f (g26 x) = f (g25 x)
@[simp] axiom s26 (x : Prop) : f (g27 x) = f (g26 x)
@[simp] axiom s27 (x : Prop) : f (g28 x) = f (g27 x)
@[simp] axiom s28 (x : Prop) : f (g29 x) = f (g28 x)
@[simp] axiom s29 (x : Prop) : f (g30 x) = f (g29 x)
@[simp] axiom s30 (x : Prop) : f (g31 x) = f (g30 x)
@[simp] axiom s31 (x : Prop) : f (g32 x) = f (g31 x)
@[simp] axiom s32 (x : Prop) : f (g33 x) = f (g32 x)
@[simp] axiom s33 (x : Prop) : f (g34 x) = f (g33 x)
@[simp] axiom s34 (x : Prop) : f (g35 x) = f (g34 x)
@[simp] axiom s35 (x : Prop) : f (g36 x) = f (g35 x)
@[simp] axiom s36 (x : Prop) : f (g37 x) = f (g36 x)
@[simp] axiom s37 (x : Prop) : f (g38 x) = f (g37 x)
@[simp] axiom s38 (x : Prop) : f (g39 x) = f (g38 x)
@[simp] axiom s39 (x : Prop) : f (g40 x) = f (g39 x)
@[simp] axiom s40 (x : Prop) : f (g41 x) = f (g40 x)
@[simp] axiom s41 (x : Prop) : f (g42 x) = f (g41 x)
@[simp] axiom s42 (x : Prop) : f (g43 x) = f (g42 x)
@[simp] axiom s43 (x : Prop) : f (g44 x) = f (g43 x)
@[simp] axiom s44 (x : Prop) : f (g45 x) = f (g44 x)
@[simp] axiom s45 (x : Prop) : f (g46 x) = f (g45 x)
@[simp] axiom s46 (x : Prop) : f (g47 x) = f (g46 x)
@[simp] axiom s47 (x : Prop) : f (g48 x) = f (g47 x)
@[simp] axiom s48 (x : Prop) : f (g49 x) = f (g48 x)
@[simp] axiom s49 (x : Prop) : f (g50 x) = f (g49 x)
@[simp] axiom s50 (x : Prop) : f (g51 x) = f (g50 x)
@[simp] axiom s51 (x : Prop) : f (g52 x) = f (g51 x)
@[simp] axiom s52 (x : Prop) : f (g53 x) = f (g52 x)
@[simp] axiom s53 (x : Prop) : f (g54 x) = f (g53 x)
@[simp] axiom s54 (x : Prop) : f (g55 x) = f (g54 x)
@[simp] axiom s55 (x : Prop) : f (g56 x) = f (g55 x)
@[simp] axiom s56 (x : Prop) : f (g57 x) = f (g56 x)
@[simp] axiom s57 (x : Prop) : f (g58 x) = f (g57 x)
@[simp] axiom s58 (x : Prop) : f (g59 x) = f (g58 x)
@[simp] axiom s59 (x : Prop) : f (g60 x) = f (g59 x)
@[simp] axiom s60 (x : Prop) : f (g61 x) = f (g60 x)
@[simp] axiom s61 (x : Prop) : f (g62 x) = f (g61 x)
@[simp] axiom s62 (x : Prop) : f (g63 x) = f (g62 x)
@[simp] axiom s63 (x : Prop) : f (g64 x) = f (g63 x)
@[simp] axiom s64 (x : Prop) : f (g65 x) = f (g64 x)
@[simp] axiom s65 (x : Prop) : f (g66 x) = f (g65 x)
@[simp] axiom s66 (x : Prop) : f (g67 x) = f (g66 x)
@[simp] axiom s67 (x : Prop) : f (g68 x) = f (g67 x)
@[simp] axiom s68 (x : Prop) : f (g69 x) = f (g68 x)
@[simp] axiom s69 (x : Prop) : f (g70 x) = f (g69 x)
@[simp] axiom s70 (x : Prop) : f (g71 x) = f (g70 x)
@[simp] axiom s71 (x : Prop) : f (g72 x) = f (g71 x)
@[simp] axiom s72 (x : Prop) : f (g73 x) = f (g72 x)
@[simp] axiom s73 (x : Prop) : f (g74 x) = f (g73 x)
@[simp] axiom s74 (x : Prop) : f (g75 x) = f (g74 x)
@[simp] axiom s75 (x : Prop) : f (g76 x) = f (g75 x)
@[simp] axiom s76 (x : Prop) : f (g77 x) = f (g76 x)
@[simp] axiom s77 (x : Prop) : f (g78 x) = f (g77 x)
@[simp] axiom s78 (x : Prop) : f (g79 x) = f (g78 x)
@[simp] axiom s79 (x : Prop) : f (g80 x) = f (g79 x)
@[simp] axiom s80 (x : Prop) : f (g81 x) = f (g80 x)
@[simp] axiom s81 (x : Prop) : f (g82 x) = f (g81 x)
@[simp] axiom s82 (x : Prop) : f (g83 x) = f (g82 x)
@[simp] axiom s83 (x : Prop) : f (g84 x) = f (g83 x)
@[simp] axiom s84 (x : Prop) : f (g85 x) = f (g84 x)
@[simp] axiom s85 (x : Prop) : f (g86 x) = f (g85 x)
@[simp] axiom s86 (x : Prop) : f (g87 x) = f (g86 x)
@[simp] axiom s87 (x : Prop) : f (g88 x) = f (g87 x)
@[simp] axiom s88 (x : Prop) : f (g89 x) = f (g88 x)
@[simp] axiom s89 (x : Prop) : f (g90 x) = f (g89 x)
@[simp] axiom s90 (x : Prop) : f (g91 x) = f (g90 x)
@[simp] axiom s91 (x : Prop) : f (g92 x) = f (g91 x)
@[simp] axiom s92 (x : Prop) : f (g93 x) = f (g92 x)
@[simp] axiom s93 (x : Prop) : f (g94 x) = f (g93 x)
@[simp] axiom s94 (x : Prop) : f (g95 x) = f (g94 x)
@[simp] axiom s95 (x : Prop) : f (g96 x) = f (g95 x)
@[simp] axiom s96 (x : Prop) : f (g97 x) = f (g96 x)
@[simp] axiom s97 (x : Prop) : f (g98 x) = f (g97 x)
@[simp] axiom s98 (x : Prop) : f (g99 x) = f (g98 x)
@[simp] axiom s99 (x : Prop) : f (g100 x) = f (g99 x)
@[simp] axiom s100 (x : Prop) : f (g101 x) = f (g100 x)
@[simp] axiom s101 (x : Prop) : f (g102 x) = f (g101 x)
@[simp] axiom s102 (x : Prop) : f (g103 x) = f (g102 x)
@[simp] axiom s103 (x : Prop) : f (g104 x) = f (g103 x)
@[simp] axiom s104 (x : Prop) : f (g105 x) = f (g104 x)
@[simp] axiom s105 (x : Prop) : f (g106 x) = f (g105 x)
@[simp] axiom s106 (x : Prop) : f (g107 x) = f (g106 x)
@[simp] axiom s107 (x : Prop) : f (g108 x) = f (g107 x)
@[simp] axiom s108 (x : Prop) : f (g109 x) = f (g108 x)
@[simp] axiom s109 (x : Prop) : f (g110 x) = f (g109 x)
@[simp] axiom s110 (x : Prop) : f (g111 x) = f (g110 x)
@[simp] axiom s111 (x : Prop) : f (g112 x) = f (g111 x)
@[simp] axiom s112 (x : Prop) : f (g113 x) = f (g112 x)
@[simp] axiom s113 (x : Prop) : f (g114 x) = f (g113 x)
@[simp] axiom s114 (x : Prop) : f (g115 x) = f (g114 x)
@[simp] axiom s115 (x : Prop) : f (g116 x) = f (g115 x)
@[simp] axiom s116 (x : Prop) : f (g117 x) = f (g116 x)
@[simp] axiom s117 (x : Prop) : f (g118 x) = f (g117 x)
@[simp] axiom s118 (x : Prop) : f (g119 x) = f (g118 x)
@[simp] axiom s119 (x : Prop) : f (g120 x) = f (g119 x)
@[simp] axiom s120 (x : Prop) : f (g121 x) = f (g120 x)
@[simp] axiom s121 (x : Prop) : f (g122 x) = f (g121 x)
@[simp] axiom s122 (x : Prop) : f (g123 x) = f (g122 x)
@[simp] axiom s123 (x : Prop) : f (g124 x) = f (g123 x)
@[simp] axiom s124 (x : Prop) : f (g125 x) = f (g124 x)
@[simp] axiom s125 (x : Prop) : f (g126 x) = f (g125 x)
@[simp] axiom s126 (x : Prop) : f (g127 x) = f (g126 x)
@[simp] axiom s127 (x : Prop) : f (g128 x) = f (g127 x)
@[simp] axiom s128 (x : Prop) : f (g129 x) = f (g128 x)
@[simp] axiom s129 (x : Prop) : f (g130 x) = f (g129 x)
@[simp] axiom s130 (x : Prop) : f (g131 x) = f (g130 x)
@[simp] axiom s131 (x : Prop) : f (g132 x) = f (g131 x)
@[simp] axiom s132 (x : Prop) : f (g133 x) = f (g132 x)
@[simp] axiom s133 (x : Prop) : f (g134 x) = f (g133 x)
@[simp] axiom s134 (x : Prop) : f (g135 x) = f (g134 x)
@[simp] axiom s135 (x : Prop) : f (g136 x) = f (g135 x)
@[simp] axiom s136 (x : Prop) : f (g137 x) = f (g136 x)
@[simp] axiom s137 (x : Prop) : f (g138 x) = f (g137 x)
@[simp] axiom s138 (x : Prop) : f (g139 x) = f (g138 x)
@[simp] axiom s139 (x : Prop) : f (g140 x) = f (g139 x)
@[simp] axiom s140 (x : Prop) : f (g141 x) = f (g140 x)
@[simp] axiom s141 (x : Prop) : f (g142 x) = f (g141 x)
@[simp] axiom s142 (x : Prop) : f (g143 x) = f (g142 x)
@[simp] axiom s143 (x : Prop) : f (g144 x) = f (g143 x)
@[simp] axiom s144 (x : Prop) : f (g145 x) = f (g144 x)
@[simp] axiom s145 (x : Prop) : f (g146 x) = f (g145 x)
@[simp] axiom s146 (x : Prop) : f (g147 x) = f (g146 x)
@[simp] axiom s147 (x : Prop) : f (g148 x) = f (g147 x)
@[simp] axiom s148 (x : Prop) : f (g149 x) = f (g148 x)
@[simp] axiom s149 (x : Prop) : f (g150 x) = f (g149 x)
@[simp] axiom s150 (x : Prop) : f (g151 x) = f (g150 x)
@[simp] axiom s151 (x : Prop) : f (g152 x) = f (g151 x)
@[simp] axiom s152 (x : Prop) : f (g153 x) = f (g152 x)
@[simp] axiom s153 (x : Prop) : f (g154 x) = f (g153 x)
@[simp] axiom s154 (x : Prop) : f (g155 x) = f (g154 x)
@[simp] axiom s155 (x : Prop) : f (g156 x) = f (g155 x)
@[simp] axiom s156 (x : Prop) : f (g157 x) = f (g156 x)
@[simp] axiom s157 (x : Prop) : f (g158 x) = f (g157 x)
@[simp] axiom s158 (x : Prop) : f (g159 x) = f (g158 x)
@[simp] axiom s159 (x : Prop) : f (g160 x) = f (g159 x)
@[simp] axiom s160 (x : Prop) : f (g161 x) = f (g160 x)
@[simp] axiom s161 (x : Prop) : f (g162 x) = f (g161 x)
@[simp] axiom s162 (x : Prop) : f (g163 x) = f (g162 x)
@[simp] axiom s163 (x : Prop) : f (g164 x) = f (g163 x)
@[simp] axiom s164 (x : Prop) : f (g165 x) = f (g164 x)
@[simp] axiom s165 (x : Prop) : f (g166 x) = f (g165 x)
@[simp] axiom s166 (x : Prop) : f (g167 x) = f (g166 x)
@[simp] axiom s167 (x : Prop) : f (g168 x) = f (g167 x)
@[simp] axiom s168 (x : Prop) : f (g169 x) = f (g168 x)
@[simp] axiom s169 (x : Prop) : f (g170 x) = f (g169 x)
@[simp] axiom s170 (x : Prop) : f (g171 x) = f (g170 x)
@[simp] axiom s171 (x : Prop) : f (g172 x) = f (g171 x)
@[simp] axiom s172 (x : Prop) : f (g173 x) = f (g172 x)
@[simp] axiom s173 (x : Prop) : f (g174 x) = f (g173 x)
@[simp] axiom s174 (x : Prop) : f (g175 x) = f (g174 x)
@[simp] axiom s175 (x : Prop) : f (g176 x) = f (g175 x)
@[simp] axiom s176 (x : Prop) : f (g177 x) = f (g176 x)
@[simp] axiom s177 (x : Prop) : f (g178 x) = f (g177 x)
@[simp] axiom s178 (x : Prop) : f (g179 x) = f (g178 x)
@[simp] axiom s179 (x : Prop) : f (g180 x) = f (g179 x)
@[simp] axiom s180 (x : Prop) : f (g181 x) = f (g180 x)
@[simp] axiom s181 (x : Prop) : f (g182 x) = f (g181 x)
@[simp] axiom s182 (x : Prop) : f (g183 x) = f (g182 x)
@[simp] axiom s183 (x : Prop) : f (g184 x) = f (g183 x)
@[simp] axiom s184 (x : Prop) : f (g185 x) = f (g184 x)
@[simp] axiom s185 (x : Prop) : f (g186 x) = f (g185 x)
@[simp] axiom s186 (x : Prop) : f (g187 x) = f (g186 x)
@[simp] axiom s187 (x : Prop) : f (g188 x) = f (g187 x)
@[simp] axiom s188 (x : Prop) : f (g189 x) = f (g188 x)
@[simp] axiom s189 (x : Prop) : f (g190 x) = f (g189 x)
@[simp] axiom s190 (x : Prop) : f (g191 x) = f (g190 x)
@[simp] axiom s191 (x : Prop) : f (g192 x) = f (g191 x)
@[simp] axiom s192 (x : Prop) : f (g193 x) = f (g192 x)
@[simp] axiom s193 (x : Prop) : f (g194 x) = f (g193 x)
@[simp] axiom s194 (x : Prop) : f (g195 x) = f (g194 x)
@[simp] axiom s195 (x : Prop) : f (g196 x) = f (g195 x)
@[simp] axiom s196 (x : Prop) : f (g197 x) = f (g196 x)
@[simp] axiom s197 (x : Prop) : f (g198 x) = f (g197 x)
@[simp] axiom s198 (x : Prop) : f (g199 x) = f (g198 x)
@[simp] axiom s199 (x : Prop) : f (g200 x) = f (g199 x)
@[simp] axiom s200 (x : Prop) : f (g201 x) = f (g200 x)
@[simp] axiom s201 (x : Prop) : f (g202 x) = f (g201 x)
@[simp] axiom s202 (x : Prop) : f (g203 x) = f (g202 x)
@[simp] axiom s203 (x : Prop) : f (g204 x) = f (g203 x)
@[simp] axiom s204 (x : Prop) : f (g205 x) = f (g204 x)
@[simp] axiom s205 (x : Prop) : f (g206 x) = f (g205 x)
@[simp] axiom s206 (x : Prop) : f (g207 x) = f (g206 x)
@[simp] axiom s207 (x : Prop) : f (g208 x) = f (g207 x)
@[simp] axiom s208 (x : Prop) : f (g209 x) = f (g208 x)
@[simp] axiom s209 (x : Prop) : f (g210 x) = f (g209 x)
@[simp] axiom s210 (x : Prop) : f (g211 x) = f (g210 x)
@[simp] axiom s211 (x : Prop) : f (g212 x) = f (g211 x)
@[simp] axiom s212 (x : Prop) : f (g213 x) = f (g212 x)
@[simp] axiom s213 (x : Prop) : f (g214 x) = f (g213 x)
@[simp] axiom s214 (x : Prop) : f (g215 x) = f (g214 x)
@[simp] axiom s215 (x : Prop) : f (g216 x) = f (g215 x)
@[simp] axiom s216 (x : Prop) : f (g217 x) = f (g216 x)
@[simp] axiom s217 (x : Prop) : f (g218 x) = f (g217 x)
@[simp] axiom s218 (x : Prop) : f (g219 x) = f (g218 x)
@[simp] axiom s219 (x : Prop) : f (g220 x) = f (g219 x)
@[simp] axiom s220 (x : Prop) : f (g221 x) = f (g220 x)
@[simp] axiom s221 (x : Prop) : f (g222 x) = f (g221 x)
@[simp] axiom s222 (x : Prop) : f (g223 x) = f (g222 x)
@[simp] axiom s223 (x : Prop) : f (g224 x) = f (g223 x)
@[simp] axiom s224 (x : Prop) : f (g225 x) = f (g224 x)
@[simp] axiom s225 (x : Prop) : f (g226 x) = f (g225 x)
@[simp] axiom s226 (x : Prop) : f (g227 x) = f (g226 x)
@[simp] axiom s227 (x : Prop) : f (g228 x) = f (g227 x)
@[simp] axiom s228 (x : Prop) : f (g229 x) = f (g228 x)
@[simp] axiom s229 (x : Prop) : f (g230 x) = f (g229 x)
@[simp] axiom s230 (x : Prop) : f (g231 x) = f (g230 x)
@[simp] axiom s231 (x : Prop) : f (g232 x) = f (g231 x)
@[simp] axiom s232 (x : Prop) : f (g233 x) = f (g232 x)
@[simp] axiom s233 (x : Prop) : f (g234 x) = f (g233 x)
@[simp] axiom s234 (x : Prop) : f (g235 x) = f (g234 x)
@[simp] axiom s235 (x : Prop) : f (g236 x) = f (g235 x)
@[simp] axiom s236 (x : Prop) : f (g237 x) = f (g236 x)
@[simp] axiom s237 (x : Prop) : f (g238 x) = f (g237 x)
@[simp] axiom s238 (x : Prop) : f (g239 x) = f (g238 x)
@[simp] axiom s239 (x : Prop) : f (g240 x) = f (g239 x)
@[simp] axiom s240 (x : Prop) : f (g241 x) = f (g240 x)
@[simp] axiom s241 (x : Prop) : f (g242 x) = f (g241 x)
@[simp] axiom s242 (x : Prop) : f (g243 x) = f (g242 x)
@[simp] axiom s243 (x : Prop) : f (g244 x) = f (g243 x)
@[simp] axiom s244 (x : Prop) : f (g245 x) = f (g244 x)
@[simp] axiom s245 (x : Prop) : f (g246 x) = f (g245 x)
@[simp] axiom s246 (x : Prop) : f (g247 x) = f (g246 x)
@[simp] axiom s247 (x : Prop) : f (g248 x) = f (g247 x)
@[simp] axiom s248 (x : Prop) : f (g249 x) = f (g248 x)
@[simp] axiom s249 (x : Prop) : f (g250 x) = f (g249 x)
@[simp] axiom s250 (x : Prop) : f (g251 x) = f (g250 x)
@[simp] axiom s251 (x : Prop) : f (g252 x) = f (g251 x)
@[simp] axiom s252 (x : Prop) : f (g253 x) = f (g252 x)
@[simp] axiom s253 (x : Prop) : f (g254 x) = f (g253 x)
@[simp] axiom s254 (x : Prop) : f (g255 x) = f (g254 x)
@[simp] axiom s255 (x : Prop) : f (g256 x) = f (g255 x)
@[simp] axiom s256 (x : Prop) : f (g257 x) = f (g256 x)
@[simp] axiom s257 (x : Prop) : f (g258 x) = f (g257 x)
@[simp] axiom s258 (x : Prop) : f (g259 x) = f (g258 x)
@[simp] axiom s259 (x : Prop) : f (g260 x) = f (g259 x)
@[simp] axiom s260 (x : Prop) : f (g261 x) = f (g260 x)
@[simp] axiom s261 (x : Prop) : f (g262 x) = f (g261 x)
@[simp] axiom s262 (x : Prop) : f (g263 x) = f (g262 x)
@[simp] axiom s263 (x : Prop) : f (g264 x) = f (g263 x)
@[simp] axiom s264 (x : Prop) : f (g265 x) = f (g264 x)
@[simp] axiom s265 (x : Prop) : f (g266 x) = f (g265 x)
@[simp] axiom s266 (x : Prop) : f (g267 x) = f (g266 x)
@[simp] axiom s267 (x : Prop) : f (g268 x) = f (g267 x)
@[simp] axiom s268 (x : Prop) : f (g269 x) = f (g268 x)
@[simp] axiom s269 (x : Prop) : f (g270 x) = f (g269 x)
@[simp] axiom s270 (x : Prop) : f (g271 x) = f (g270 x)
@[simp] axiom s271 (x : Prop) : f (g272 x) = f (g271 x)
@[simp] axiom s272 (x : Prop) : f (g273 x) = f (g272 x)
@[simp] axiom s273 (x : Prop) : f (g274 x) = f (g273 x)
@[simp] axiom s274 (x : Prop) : f (g275 x) = f (g274 x)
@[simp] axiom s275 (x : Prop) : f (g276 x) = f (g275 x)
@[simp] axiom s276 (x : Prop) : f (g277 x) = f (g276 x)
@[simp] axiom s277 (x : Prop) : f (g278 x) = f (g277 x)
@[simp] axiom s278 (x : Prop) : f (g279 x) = f (g278 x)
@[simp] axiom s279 (x : Prop) : f (g280 x) = f (g279 x)
@[simp] axiom s280 (x : Prop) : f (g281 x) = f (g280 x)
@[simp] axiom s281 (x : Prop) : f (g282 x) = f (g281 x)
@[simp] axiom s282 (x : Prop) : f (g283 x) = f (g282 x)
@[simp] axiom s283 (x : Prop) : f (g284 x) = f (g283 x)
@[simp] axiom s284 (x : Prop) : f (g285 x) = f (g284 x)
@[simp] axiom s285 (x : Prop) : f (g286 x) = f (g285 x)
@[simp] axiom s286 (x : Prop) : f (g287 x) = f (g286 x)
@[simp] axiom s287 (x : Prop) : f (g288 x) = f (g287 x)
@[simp] axiom s288 (x : Prop) : f (g289 x) = f (g288 x)
@[simp] axiom s289 (x : Prop) : f (g290 x) = f (g289 x)
@[simp] axiom s290 (x : Prop) : f (g291 x) = f (g290 x)
@[simp] axiom s291 (x : Prop) : f (g292 x) = f (g291 x)
@[simp] axiom s292 (x : Prop) : f (g293 x) = f (g292 x)
@[simp] axiom s293 (x : Prop) : f (g294 x) = f (g293 x)
@[simp] axiom s294 (x : Prop) : f (g295 x) = f (g294 x)
@[simp] axiom s295 (x : Prop) : f (g296 x) = f (g295 x)
@[simp] axiom s296 (x : Prop) : f (g297 x) = f (g296 x)
@[simp] axiom s297 (x : Prop) : f (g298 x) = f (g297 x)
@[simp] axiom s298 (x : Prop) : f (g299 x) = f (g298 x)
@[simp] axiom s299 (x : Prop) : f (g300 x) = f (g299 x)
@[simp] axiom s300 (x : Prop) : f (g301 x) = f (g300 x)
@[simp] axiom s301 (x : Prop) : f (g302 x) = f (g301 x)
@[simp] axiom s302 (x : Prop) : f (g303 x) = f (g302 x)
@[simp] axiom s303 (x : Prop) : f (g304 x) = f (g303 x)
@[simp] axiom s304 (x : Prop) : f (g305 x) = f (g304 x)
@[simp] axiom s305 (x : Prop) : f (g306 x) = f (g305 x)
@[simp] axiom s306 (x : Prop) : f (g307 x) = f (g306 x)
@[simp] axiom s307 (x : Prop) : f (g308 x) = f (g307 x)
@[simp] axiom s308 (x : Prop) : f (g309 x) = f (g308 x)
@[simp] axiom s309 (x : Prop) : f (g310 x) = f (g309 x)
@[simp] axiom s310 (x : Prop) : f (g311 x) = f (g310 x)
@[simp] axiom s311 (x : Prop) : f (g312 x) = f (g311 x)
@[simp] axiom s312 (x : Prop) : f (g313 x) = f (g312 x)
@[simp] axiom s313 (x : Prop) : f (g314 x) = f (g313 x)
@[simp] axiom s314 (x : Prop) : f (g315 x) = f (g314 x)
@[simp] axiom s315 (x : Prop) : f (g316 x) = f (g315 x)
@[simp] axiom s316 (x : Prop) : f (g317 x) = f (g316 x)
@[simp] axiom s317 (x : Prop) : f (g318 x) = f (g317 x)
@[simp] axiom s318 (x : Prop) : f (g319 x) = f (g318 x)
@[simp] axiom s319 (x : Prop) : f (g320 x) = f (g319 x)
@[simp] axiom s320 (x : Prop) : f (g321 x) = f (g320 x)
@[simp] axiom s321 (x : Prop) : f (g322 x) = f (g321 x)
@[simp] axiom s322 (x : Prop) : f (g323 x) = f (g322 x)
@[simp] axiom s323 (x : Prop) : f (g324 x) = f (g323 x)
@[simp] axiom s324 (x : Prop) : f (g325 x) = f (g324 x)
@[simp] axiom s325 (x : Prop) : f (g326 x) = f (g325 x)
@[simp] axiom s326 (x : Prop) : f (g327 x) = f (g326 x)
@[simp] axiom s327 (x : Prop) : f (g328 x) = f (g327 x)
@[simp] axiom s328 (x : Prop) : f (g329 x) = f (g328 x)
@[simp] axiom s329 (x : Prop) : f (g330 x) = f (g329 x)
@[simp] axiom s330 (x : Prop) : f (g331 x) = f (g330 x)
@[simp] axiom s331 (x : Prop) : f (g332 x) = f (g331 x)
@[simp] axiom s332 (x : Prop) : f (g333 x) = f (g332 x)
@[simp] axiom s333 (x : Prop) : f (g334 x) = f (g333 x)
@[simp] axiom s334 (x : Prop) : f (g335 x) = f (g334 x)
@[simp] axiom s335 (x : Prop) : f (g336 x) = f (g335 x)
@[simp] axiom s336 (x : Prop) : f (g337 x) = f (g336 x)
@[simp] axiom s337 (x : Prop) : f (g338 x) = f (g337 x)
@[simp] axiom s338 (x : Prop) : f (g339 x) = f (g338 x)
@[simp] axiom s339 (x : Prop) : f (g340 x) = f (g339 x)
@[simp] axiom s340 (x : Prop) : f (g341 x) = f (g340 x)
@[simp] axiom s341 (x : Prop) : f (g342 x) = f (g341 x)
@[simp] axiom s342 (x : Prop) : f (g343 x) = f (g342 x)
@[simp] axiom s343 (x : Prop) : f (g344 x) = f (g343 x)
@[simp] axiom s344 (x : Prop) : f (g345 x) = f (g344 x)
@[simp] axiom s345 (x : Prop) : f (g346 x) = f (g345 x)
@[simp] axiom s346 (x : Prop) : f (g347 x) = f (g346 x)
@[simp] axiom s347 (x : Prop) : f (g348 x) = f (g347 x)
@[simp] axiom s348 (x : Prop) : f (g349 x) = f (g348 x)
@[simp] axiom s349 (x : Prop) : f (g350 x) = f (g349 x)
@[simp] axiom s350 (x : Prop) : f (g351 x) = f (g350 x)
@[simp] axiom s351 (x : Prop) : f (g352 x) = f (g351 x)
@[simp] axiom s352 (x : Prop) : f (g353 x) = f (g352 x)
@[simp] axiom s353 (x : Prop) : f (g354 x) = f (g353 x)
@[simp] axiom s354 (x : Prop) : f (g355 x) = f (g354 x)
@[simp] axiom s355 (x : Prop) : f (g356 x) = f (g355 x)
@[simp] axiom s356 (x : Prop) : f (g357 x) = f (g356 x)
@[simp] axiom s357 (x : Prop) : f (g358 x) = f (g357 x)
@[simp] axiom s358 (x : Prop) : f (g359 x) = f (g358 x)
@[simp] axiom s359 (x : Prop) : f (g360 x) = f (g359 x)
@[simp] axiom s360 (x : Prop) : f (g361 x) = f (g360 x)
@[simp] axiom s361 (x : Prop) : f (g362 x) = f (g361 x)
@[simp] axiom s362 (x : Prop) : f (g363 x) = f (g362 x)
@[simp] axiom s363 (x : Prop) : f (g364 x) = f (g363 x)
@[simp] axiom s364 (x : Prop) : f (g365 x) = f (g364 x)
@[simp] axiom s365 (x : Prop) : f (g366 x) = f (g365 x)
@[simp] axiom s366 (x : Prop) : f (g367 x) = f (g366 x)
@[simp] axiom s367 (x : Prop) : f (g368 x) = f (g367 x)
@[simp] axiom s368 (x : Prop) : f (g369 x) = f (g368 x)
@[simp] axiom s369 (x : Prop) : f (g370 x) = f (g369 x)
@[simp] axiom s370 (x : Prop) : f (g371 x) = f (g370 x)
@[simp] axiom s371 (x : Prop) : f (g372 x) = f (g371 x)
@[simp] axiom s372 (x : Prop) : f (g373 x) = f (g372 x)
@[simp] axiom s373 (x : Prop) : f (g374 x) = f (g373 x)
@[simp] axiom s374 (x : Prop) : f (g375 x) = f (g374 x)
@[simp] axiom s375 (x : Prop) : f (g376 x) = f (g375 x)
@[simp] axiom s376 (x : Prop) : f (g377 x) = f (g376 x)
@[simp] axiom s377 (x : Prop) : f (g378 x) = f (g377 x)
@[simp] axiom s378 (x : Prop) : f (g379 x) = f (g378 x)
@[simp] axiom s379 (x : Prop) : f (g380 x) = f (g379 x)
@[simp] axiom s380 (x : Prop) : f (g381 x) = f (g380 x)
@[simp] axiom s381 (x : Prop) : f (g382 x) = f (g381 x)
@[simp] axiom s382 (x : Prop) : f (g383 x) = f (g382 x)
@[simp] axiom s383 (x : Prop) : f (g384 x) = f (g383 x)
@[simp] axiom s384 (x : Prop) : f (g385 x) = f (g384 x)
@[simp] axiom s385 (x : Prop) : f (g386 x) = f (g385 x)
@[simp] axiom s386 (x : Prop) : f (g387 x) = f (g386 x)
@[simp] axiom s387 (x : Prop) : f (g388 x) = f (g387 x)
@[simp] axiom s388 (x : Prop) : f (g389 x) = f (g388 x)
@[simp] axiom s389 (x : Prop) : f (g390 x) = f (g389 x)
@[simp] axiom s390 (x : Prop) : f (g391 x) = f (g390 x)
@[simp] axiom s391 (x : Prop) : f (g392 x) = f (g391 x)
@[simp] axiom s392 (x : Prop) : f (g393 x) = f (g392 x)
@[simp] axiom s393 (x : Prop) : f (g394 x) = f (g393 x)
@[simp] axiom s394 (x : Prop) : f (g395 x) = f (g394 x)
@[simp] axiom s395 (x : Prop) : f (g396 x) = f (g395 x)
@[simp] axiom s396 (x : Prop) : f (g397 x) = f (g396 x)
@[simp] axiom s397 (x : Prop) : f (g398 x) = f (g397 x)
@[simp] axiom s398 (x : Prop) : f (g399 x) = f (g398 x)
@[simp] axiom s399 (x : Prop) : f (g400 x) = f (g399 x)
@[simp] axiom s400 (x : Prop) : f (g401 x) = f (g400 x)
@[simp] axiom s401 (x : Prop) : f (g402 x) = f (g401 x)
@[simp] axiom s402 (x : Prop) : f (g403 x) = f (g402 x)
@[simp] axiom s403 (x : Prop) : f (g404 x) = f (g403 x)
@[simp] axiom s404 (x : Prop) : f (g405 x) = f (g404 x)
@[simp] axiom s405 (x : Prop) : f (g406 x) = f (g405 x)
@[simp] axiom s406 (x : Prop) : f (g407 x) = f (g406 x)
@[simp] axiom s407 (x : Prop) : f (g408 x) = f (g407 x)
@[simp] axiom s408 (x : Prop) : f (g409 x) = f (g408 x)
@[simp] axiom s409 (x : Prop) : f (g410 x) = f (g409 x)
@[simp] axiom s410 (x : Prop) : f (g411 x) = f (g410 x)
@[simp] axiom s411 (x : Prop) : f (g412 x) = f (g411 x)
@[simp] axiom s412 (x : Prop) : f (g413 x) = f (g412 x)
@[simp] axiom s413 (x : Prop) : f (g414 x) = f (g413 x)
@[simp] axiom s414 (x : Prop) : f (g415 x) = f (g414 x)
@[simp] axiom s415 (x : Prop) : f (g416 x) = f (g415 x)
@[simp] axiom s416 (x : Prop) : f (g417 x) = f (g416 x)
@[simp] axiom s417 (x : Prop) : f (g418 x) = f (g417 x)
@[simp] axiom s418 (x : Prop) : f (g419 x) = f (g418 x)
@[simp] axiom s419 (x : Prop) : f (g420 x) = f (g419 x)
@[simp] axiom s420 (x : Prop) : f (g421 x) = f (g420 x)
@[simp] axiom s421 (x : Prop) : f (g422 x) = f (g421 x)
@[simp] axiom s422 (x : Prop) : f (g423 x) = f (g422 x)
@[simp] axiom s423 (x : Prop) : f (g424 x) = f (g423 x)
@[simp] axiom s424 (x : Prop) : f (g425 x) = f (g424 x)
@[simp] axiom s425 (x : Prop) : f (g426 x) = f (g425 x)
@[simp] axiom s426 (x : Prop) : f (g427 x) = f (g426 x)
@[simp] axiom s427 (x : Prop) : f (g428 x) = f (g427 x)
@[simp] axiom s428 (x : Prop) : f (g429 x) = f (g428 x)
@[simp] axiom s429 (x : Prop) : f (g430 x) = f (g429 x)
@[simp] axiom s430 (x : Prop) : f (g431 x) = f (g430 x)
@[simp] axiom s431 (x : Prop) : f (g432 x) = f (g431 x)
@[simp] axiom s432 (x : Prop) : f (g433 x) = f (g432 x)
@[simp] axiom s433 (x : Prop) : f (g434 x) = f (g433 x)
@[simp] axiom s434 (x : Prop) : f (g435 x) = f (g434 x)
@[simp] axiom s435 (x : Prop) : f (g436 x) = f (g435 x)
@[simp] axiom s436 (x : Prop) : f (g437 x) = f (g436 x)
@[simp] axiom s437 (x : Prop) : f (g438 x) = f (g437 x)
@[simp] axiom s438 (x : Prop) : f (g439 x) = f (g438 x)
@[simp] axiom s439 (x : Prop) : f (g440 x) = f (g439 x)
@[simp] axiom s440 (x : Prop) : f (g441 x) = f (g440 x)
@[simp] axiom s441 (x : Prop) : f (g442 x) = f (g441 x)
@[simp] axiom s442 (x : Prop) : f (g443 x) = f (g442 x)
@[simp] axiom s443 (x : Prop) : f (g444 x) = f (g443 x)
@[simp] axiom s444 (x : Prop) : f (g445 x) = f (g444 x)
@[simp] axiom s445 (x : Prop) : f (g446 x) = f (g445 x)
@[simp] axiom s446 (x : Prop) : f (g447 x) = f (g446 x)
@[simp] axiom s447 (x : Prop) : f (g448 x) = f (g447 x)
@[simp] axiom s448 (x : Prop) : f (g449 x) = f (g448 x)
@[simp] axiom s449 (x : Prop) : f (g450 x) = f (g449 x)
@[simp] axiom s450 (x : Prop) : f (g451 x) = f (g450 x)
@[simp] axiom s451 (x : Prop) : f (g452 x) = f (g451 x)
@[simp] axiom s452 (x : Prop) : f (g453 x) = f (g452 x)
@[simp] axiom s453 (x : Prop) : f (g454 x) = f (g453 x)
@[simp] axiom s454 (x : Prop) : f (g455 x) = f (g454 x)
@[simp] axiom s455 (x : Prop) : f (g456 x) = f (g455 x)
@[simp] axiom s456 (x : Prop) : f (g457 x) = f (g456 x)
@[simp] axiom s457 (x : Prop) : f (g458 x) = f (g457 x)
@[simp] axiom s458 (x : Prop) : f (g459 x) = f (g458 x)
@[simp] axiom s459 (x : Prop) : f (g460 x) = f (g459 x)
@[simp] axiom s460 (x : Prop) : f (g461 x) = f (g460 x)
@[simp] axiom s461 (x : Prop) : f (g462 x) = f (g461 x)
@[simp] axiom s462 (x : Prop) : f (g463 x) = f (g462 x)
@[simp] axiom s463 (x : Prop) : f (g464 x) = f (g463 x)
@[simp] axiom s464 (x : Prop) : f (g465 x) = f (g464 x)
@[simp] axiom s465 (x : Prop) : f (g466 x) = f (g465 x)
@[simp] axiom s466 (x : Prop) : f (g467 x) = f (g466 x)
@[simp] axiom s467 (x : Prop) : f (g468 x) = f (g467 x)
@[simp] axiom s468 (x : Prop) : f (g469 x) = f (g468 x)
@[simp] axiom s469 (x : Prop) : f (g470 x) = f (g469 x)
@[simp] axiom s470 (x : Prop) : f (g471 x) = f (g470 x)
@[simp] axiom s471 (x : Prop) : f (g472 x) = f (g471 x)
@[simp] axiom s472 (x : Prop) : f (g473 x) = f (g472 x)
@[simp] axiom s473 (x : Prop) : f (g474 x) = f (g473 x)
@[simp] axiom s474 (x : Prop) : f (g475 x) = f (g474 x)
@[simp] axiom s475 (x : Prop) : f (g476 x) = f (g475 x)
@[simp] axiom s476 (x : Prop) : f (g477 x) = f (g476 x)
@[simp] axiom s477 (x : Prop) : f (g478 x) = f (g477 x)
@[simp] axiom s478 (x : Prop) : f (g479 x) = f (g478 x)
@[simp] axiom s479 (x : Prop) : f (g480 x) = f (g479 x)
@[simp] axiom s480 (x : Prop) : f (g481 x) = f (g480 x)
@[simp] axiom s481 (x : Prop) : f (g482 x) = f (g481 x)
@[simp] axiom s482 (x : Prop) : f (g483 x) = f (g482 x)
@[simp] axiom s483 (x : Prop) : f (g484 x) = f (g483 x)
@[simp] axiom s484 (x : Prop) : f (g485 x) = f (g484 x)
@[simp] axiom s485 (x : Prop) : f (g486 x) = f (g485 x)
@[simp] axiom s486 (x : Prop) : f (g487 x) = f (g486 x)
@[simp] axiom s487 (x : Prop) : f (g488 x) = f (g487 x)
@[simp] axiom s488 (x : Prop) : f (g489 x) = f (g488 x)
@[simp] axiom s489 (x : Prop) : f (g490 x) = f (g489 x)
@[simp] axiom s490 (x : Prop) : f (g491 x) = f (g490 x)
@[simp] axiom s491 (x : Prop) : f (g492 x) = f (g491 x)
@[simp] axiom s492 (x : Prop) : f (g493 x) = f (g492 x)
@[simp] axiom s493 (x : Prop) : f (g494 x) = f (g493 x)
@[simp] axiom s494 (x : Prop) : f (g495 x) = f (g494 x)
@[simp] axiom s495 (x : Prop) : f (g496 x) = f (g495 x)
@[simp] axiom s496 (x : Prop) : f (g497 x) = f (g496 x)
@[simp] axiom s497 (x : Prop) : f (g498 x) = f (g497 x)
@[simp] axiom s498 (x : Prop) : f (g499 x) = f (g498 x)
@[simp] axiom s499 (x : Prop) : f (g500 x) = f (g499 x)
@[simp] axiom s500 (x : Prop) : f (g501 x) = f (g500 x)
@[simp] axiom s501 (x : Prop) : f (g502 x) = f (g501 x)
@[simp] axiom s502 (x : Prop) : f (g503 x) = f (g502 x)
@[simp] axiom s503 (x : Prop) : f (g504 x) = f (g503 x)
@[simp] axiom s504 (x : Prop) : f (g505 x) = f (g504 x)
@[simp] axiom s505 (x : Prop) : f (g506 x) = f (g505 x)
@[simp] axiom s506 (x : Prop) : f (g507 x) = f (g506 x)
@[simp] axiom s507 (x : Prop) : f (g508 x) = f (g507 x)
@[simp] axiom s508 (x : Prop) : f (g509 x) = f (g508 x)
@[simp] axiom s509 (x : Prop) : f (g510 x) = f (g509 x)
@[simp] axiom s510 (x : Prop) : f (g511 x) = f (g510 x)
@[simp] axiom s511 (x : Prop) : f (g512 x) = f (g511 x)
@[simp] axiom s512 (x : Prop) : f (g513 x) = f (g512 x)
@[simp] axiom s513 (x : Prop) : f (g514 x) = f (g513 x)
@[simp] axiom s514 (x : Prop) : f (g515 x) = f (g514 x)
@[simp] axiom s515 (x : Prop) : f (g516 x) = f (g515 x)
@[simp] axiom s516 (x : Prop) : f (g517 x) = f (g516 x)
@[simp] axiom s517 (x : Prop) : f (g518 x) = f (g517 x)
@[simp] axiom s518 (x : Prop) : f (g519 x) = f (g518 x)
@[simp] axiom s519 (x : Prop) : f (g520 x) = f (g519 x)
@[simp] axiom s520 (x : Prop) : f (g521 x) = f (g520 x)
@[simp] axiom s521 (x : Prop) : f (g522 x) = f (g521 x)
@[simp] axiom s522 (x : Prop) : f (g523 x) = f (g522 x)
@[simp] axiom s523 (x : Prop) : f (g524 x) = f (g523 x)
@[simp] axiom s524 (x : Prop) : f (g525 x) = f (g524 x)
@[simp] axiom s525 (x : Prop) : f (g526 x) = f (g525 x)
@[simp] axiom s526 (x : Prop) : f (g527 x) = f (g526 x)
@[simp] axiom s527 (x : Prop) : f (g528 x) = f (g527 x)
@[simp] axiom s528 (x : Prop) : f (g529 x) = f (g528 x)
@[simp] axiom s529 (x : Prop) : f (g530 x) = f (g529 x)
@[simp] axiom s530 (x : Prop) : f (g531 x) = f (g530 x)
@[simp] axiom s531 (x : Prop) : f (g532 x) = f (g531 x)
@[simp] axiom s532 (x : Prop) : f (g533 x) = f (g532 x)
@[simp] axiom s533 (x : Prop) : f (g534 x) = f (g533 x)
@[simp] axiom s534 (x : Prop) : f (g535 x) = f (g534 x)
@[simp] axiom s535 (x : Prop) : f (g536 x) = f (g535 x)
@[simp] axiom s536 (x : Prop) : f (g537 x) = f (g536 x)
@[simp] axiom s537 (x : Prop) : f (g538 x) = f (g537 x)
@[simp] axiom s538 (x : Prop) : f (g539 x) = f (g538 x)
@[simp] axiom s539 (x : Prop) : f (g540 x) = f (g539 x)
@[simp] axiom s540 (x : Prop) : f (g541 x) = f (g540 x)
@[simp] axiom s541 (x : Prop) : f (g542 x) = f (g541 x)
@[simp] axiom s542 (x : Prop) : f (g543 x) = f (g542 x)
@[simp] axiom s543 (x : Prop) : f (g544 x) = f (g543 x)
@[simp] axiom s544 (x : Prop) : f (g545 x) = f (g544 x)
@[simp] axiom s545 (x : Prop) : f (g546 x) = f (g545 x)
@[simp] axiom s546 (x : Prop) : f (g547 x) = f (g546 x)
@[simp] axiom s547 (x : Prop) : f (g548 x) = f (g547 x)
@[simp] axiom s548 (x : Prop) : f (g549 x) = f (g548 x)
@[simp] axiom s549 (x : Prop) : f (g550 x) = f (g549 x)
@[simp] axiom s550 (x : Prop) : f (g551 x) = f (g550 x)
@[simp] axiom s551 (x : Prop) : f (g552 x) = f (g551 x)
@[simp] axiom s552 (x : Prop) : f (g553 x) = f (g552 x)
@[simp] axiom s553 (x : Prop) : f (g554 x) = f (g553 x)
@[simp] axiom s554 (x : Prop) : f (g555 x) = f (g554 x)
@[simp] axiom s555 (x : Prop) : f (g556 x) = f (g555 x)
@[simp] axiom s556 (x : Prop) : f (g557 x) = f (g556 x)
@[simp] axiom s557 (x : Prop) : f (g558 x) = f (g557 x)
@[simp] axiom s558 (x : Prop) : f (g559 x) = f (g558 x)
@[simp] axiom s559 (x : Prop) : f (g560 x) = f (g559 x)
@[simp] axiom s560 (x : Prop) : f (g561 x) = f (g560 x)
@[simp] axiom s561 (x : Prop) : f (g562 x) = f (g561 x)
@[simp] axiom s562 (x : Prop) : f (g563 x) = f (g562 x)
@[simp] axiom s563 (x : Prop) : f (g564 x) = f (g563 x)
@[simp] axiom s564 (x : Prop) : f (g565 x) = f (g564 x)
@[simp] axiom s565 (x : Prop) : f (g566 x) = f (g565 x)
@[simp] axiom s566 (x : Prop) : f (g567 x) = f (g566 x)
@[simp] axiom s567 (x : Prop) : f (g568 x) = f (g567 x)
@[simp] axiom s568 (x : Prop) : f (g569 x) = f (g568 x)
@[simp] axiom s569 (x : Prop) : f (g570 x) = f (g569 x)
@[simp] axiom s570 (x : Prop) : f (g571 x) = f (g570 x)
@[simp] axiom s571 (x : Prop) : f (g572 x) = f (g571 x)
@[simp] axiom s572 (x : Prop) : f (g573 x) = f (g572 x)
@[simp] axiom s573 (x : Prop) : f (g574 x) = f (g573 x)
@[simp] axiom s574 (x : Prop) : f (g575 x) = f (g574 x)
@[simp] axiom s575 (x : Prop) : f (g576 x) = f (g575 x)
@[simp] axiom s576 (x : Prop) : f (g577 x) = f (g576 x)
@[simp] axiom s577 (x : Prop) : f (g578 x) = f (g577 x)
@[simp] axiom s578 (x : Prop) : f (g579 x) = f (g578 x)
@[simp] axiom s579 (x : Prop) : f (g580 x) = f (g579 x)
@[simp] axiom s580 (x : Prop) : f (g581 x) = f (g580 x)
@[simp] axiom s581 (x : Prop) : f (g582 x) = f (g581 x)
@[simp] axiom s582 (x : Prop) : f (g583 x) = f (g582 x)
@[simp] axiom s583 (x : Prop) : f (g584 x) = f (g583 x)
@[simp] axiom s584 (x : Prop) : f (g585 x) = f (g584 x)
@[simp] axiom s585 (x : Prop) : f (g586 x) = f (g585 x)
@[simp] axiom s586 (x : Prop) : f (g587 x) = f (g586 x)
@[simp] axiom s587 (x : Prop) : f (g588 x) = f (g587 x)
@[simp] axiom s588 (x : Prop) : f (g589 x) = f (g588 x)
@[simp] axiom s589 (x : Prop) : f (g590 x) = f (g589 x)
@[simp] axiom s590 (x : Prop) : f (g591 x) = f (g590 x)
@[simp] axiom s591 (x : Prop) : f (g592 x) = f (g591 x)
@[simp] axiom s592 (x : Prop) : f (g593 x) = f (g592 x)
@[simp] axiom s593 (x : Prop) : f (g594 x) = f (g593 x)
@[simp] axiom s594 (x : Prop) : f (g595 x) = f (g594 x)
@[simp] axiom s595 (x : Prop) : f (g596 x) = f (g595 x)
@[simp] axiom s596 (x : Prop) : f (g597 x) = f (g596 x)
@[simp] axiom s597 (x : Prop) : f (g598 x) = f (g597 x)
@[simp] axiom s598 (x : Prop) : f (g599 x) = f (g598 x)
@[simp] axiom s599 (x : Prop) : f (g600 x) = f (g599 x)
@[simp] axiom s600 (x : Prop) : f (g601 x) = f (g600 x)
@[simp] axiom s601 (x : Prop) : f (g602 x) = f (g601 x)
@[simp] axiom s602 (x : Prop) : f (g603 x) = f (g602 x)
@[simp] axiom s603 (x : Prop) : f (g604 x) = f (g603 x)
@[simp] axiom s604 (x : Prop) : f (g605 x) = f (g604 x)
@[simp] axiom s605 (x : Prop) : f (g606 x) = f (g605 x)
@[simp] axiom s606 (x : Prop) : f (g607 x) = f (g606 x)
@[simp] axiom s607 (x : Prop) : f (g608 x) = f (g607 x)
@[simp] axiom s608 (x : Prop) : f (g609 x) = f (g608 x)
@[simp] axiom s609 (x : Prop) : f (g610 x) = f (g609 x)
@[simp] axiom s610 (x : Prop) : f (g611 x) = f (g610 x)
@[simp] axiom s611 (x : Prop) : f (g612 x) = f (g611 x)
@[simp] axiom s612 (x : Prop) : f (g613 x) = f (g612 x)
@[simp] axiom s613 (x : Prop) : f (g614 x) = f (g613 x)
@[simp] axiom s614 (x : Prop) : f (g615 x) = f (g614 x)
@[simp] axiom s615 (x : Prop) : f (g616 x) = f (g615 x)
@[simp] axiom s616 (x : Prop) : f (g617 x) = f (g616 x)
@[simp] axiom s617 (x : Prop) : f (g618 x) = f (g617 x)
@[simp] axiom s618 (x : Prop) : f (g619 x) = f (g618 x)
@[simp] axiom s619 (x : Prop) : f (g620 x) = f (g619 x)
@[simp] axiom s620 (x : Prop) : f (g621 x) = f (g620 x)
@[simp] axiom s621 (x : Prop) : f (g622 x) = f (g621 x)
@[simp] axiom s622 (x : Prop) : f (g623 x) = f (g622 x)
@[simp] axiom s623 (x : Prop) : f (g624 x) = f (g623 x)
@[simp] axiom s624 (x : Prop) : f (g625 x) = f (g624 x)
@[simp] axiom s625 (x : Prop) : f (g626 x) = f (g625 x)
@[simp] axiom s626 (x : Prop) : f (g627 x) = f (g626 x)
@[simp] axiom s627 (x : Prop) : f (g628 x) = f (g627 x)
@[simp] axiom s628 (x : Prop) : f (g629 x) = f (g628 x)
@[simp] axiom s629 (x : Prop) : f (g630 x) = f (g629 x)
@[simp] axiom s630 (x : Prop) : f (g631 x) = f (g630 x)
@[simp] axiom s631 (x : Prop) : f (g632 x) = f (g631 x)
@[simp] axiom s632 (x : Prop) : f (g633 x) = f (g632 x)
@[simp] axiom s633 (x : Prop) : f (g634 x) = f (g633 x)
@[simp] axiom s634 (x : Prop) : f (g635 x) = f (g634 x)
@[simp] axiom s635 (x : Prop) : f (g636 x) = f (g635 x)
@[simp] axiom s636 (x : Prop) : f (g637 x) = f (g636 x)
@[simp] axiom s637 (x : Prop) : f (g638 x) = f (g637 x)
@[simp] axiom s638 (x : Prop) : f (g639 x) = f (g638 x)
@[simp] axiom s639 (x : Prop) : f (g640 x) = f (g639 x)
@[simp] axiom s640 (x : Prop) : f (g641 x) = f (g640 x)
@[simp] axiom s641 (x : Prop) : f (g642 x) = f (g641 x)
@[simp] axiom s642 (x : Prop) : f (g643 x) = f (g642 x)
@[simp] axiom s643 (x : Prop) : f (g644 x) = f (g643 x)
@[simp] axiom s644 (x : Prop) : f (g645 x) = f (g644 x)
@[simp] axiom s645 (x : Prop) : f (g646 x) = f (g645 x)
@[simp] axiom s646 (x : Prop) : f (g647 x) = f (g646 x)
@[simp] axiom s647 (x : Prop) : f (g648 x) = f (g647 x)
@[simp] axiom s648 (x : Prop) : f (g649 x) = f (g648 x)
@[simp] axiom s649 (x : Prop) : f (g650 x) = f (g649 x)
@[simp] axiom s650 (x : Prop) : f (g651 x) = f (g650 x)
@[simp] axiom s651 (x : Prop) : f (g652 x) = f (g651 x)
@[simp] axiom s652 (x : Prop) : f (g653 x) = f (g652 x)
@[simp] axiom s653 (x : Prop) : f (g654 x) = f (g653 x)
@[simp] axiom s654 (x : Prop) : f (g655 x) = f (g654 x)
@[simp] axiom s655 (x : Prop) : f (g656 x) = f (g655 x)
@[simp] axiom s656 (x : Prop) : f (g657 x) = f (g656 x)
@[simp] axiom s657 (x : Prop) : f (g658 x) = f (g657 x)
@[simp] axiom s658 (x : Prop) : f (g659 x) = f (g658 x)
@[simp] axiom s659 (x : Prop) : f (g660 x) = f (g659 x)
@[simp] axiom s660 (x : Prop) : f (g661 x) = f (g660 x)
@[simp] axiom s661 (x : Prop) : f (g662 x) = f (g661 x)
@[simp] axiom s662 (x : Prop) : f (g663 x) = f (g662 x)
@[simp] axiom s663 (x : Prop) : f (g664 x) = f (g663 x)
@[simp] axiom s664 (x : Prop) : f (g665 x) = f (g664 x)
@[simp] axiom s665 (x : Prop) : f (g666 x) = f (g665 x)
@[simp] axiom s666 (x : Prop) : f (g667 x) = f (g666 x)
@[simp] axiom s667 (x : Prop) : f (g668 x) = f (g667 x)
@[simp] axiom s668 (x : Prop) : f (g669 x) = f (g668 x)
@[simp] axiom s669 (x : Prop) : f (g670 x) = f (g669 x)
@[simp] axiom s670 (x : Prop) : f (g671 x) = f (g670 x)
@[simp] axiom s671 (x : Prop) : f (g672 x) = f (g671 x)
@[simp] axiom s672 (x : Prop) : f (g673 x) = f (g672 x)
@[simp] axiom s673 (x : Prop) : f (g674 x) = f (g673 x)
@[simp] axiom s674 (x : Prop) : f (g675 x) = f (g674 x)
@[simp] axiom s675 (x : Prop) : f (g676 x) = f (g675 x)
@[simp] axiom s676 (x : Prop) : f (g677 x) = f (g676 x)
@[simp] axiom s677 (x : Prop) : f (g678 x) = f (g677 x)
@[simp] axiom s678 (x : Prop) : f (g679 x) = f (g678 x)
@[simp] axiom s679 (x : Prop) : f (g680 x) = f (g679 x)
@[simp] axiom s680 (x : Prop) : f (g681 x) = f (g680 x)
@[simp] axiom s681 (x : Prop) : f (g682 x) = f (g681 x)
@[simp] axiom s682 (x : Prop) : f (g683 x) = f (g682 x)
@[simp] axiom s683 (x : Prop) : f (g684 x) = f (g683 x)
@[simp] axiom s684 (x : Prop) : f (g685 x) = f (g684 x)
@[simp] axiom s685 (x : Prop) : f (g686 x) = f (g685 x)
@[simp] axiom s686 (x : Prop) : f (g687 x) = f (g686 x)
@[simp] axiom s687 (x : Prop) : f (g688 x) = f (g687 x)
@[simp] axiom s688 (x : Prop) : f (g689 x) = f (g688 x)
@[simp] axiom s689 (x : Prop) : f (g690 x) = f (g689 x)
@[simp] axiom s690 (x : Prop) : f (g691 x) = f (g690 x)
@[simp] axiom s691 (x : Prop) : f (g692 x) = f (g691 x)
@[simp] axiom s692 (x : Prop) : f (g693 x) = f (g692 x)
@[simp] axiom s693 (x : Prop) : f (g694 x) = f (g693 x)
@[simp] axiom s694 (x : Prop) : f (g695 x) = f (g694 x)
@[simp] axiom s695 (x : Prop) : f (g696 x) = f (g695 x)
@[simp] axiom s696 (x : Prop) : f (g697 x) = f (g696 x)
@[simp] axiom s697 (x : Prop) : f (g698 x) = f (g697 x)
@[simp] axiom s698 (x : Prop) : f (g699 x) = f (g698 x)
@[simp] axiom s699 (x : Prop) : f (g700 x) = f (g699 x)
@[simp] axiom s700 (x : Prop) : f (g701 x) = f (g700 x)
@[simp] axiom s701 (x : Prop) : f (g702 x) = f (g701 x)
@[simp] axiom s702 (x : Prop) : f (g703 x) = f (g702 x)
@[simp] axiom s703 (x : Prop) : f (g704 x) = f (g703 x)
@[simp] axiom s704 (x : Prop) : f (g705 x) = f (g704 x)
@[simp] axiom s705 (x : Prop) : f (g706 x) = f (g705 x)
@[simp] axiom s706 (x : Prop) : f (g707 x) = f (g706 x)
@[simp] axiom s707 (x : Prop) : f (g708 x) = f (g707 x)
@[simp] axiom s708 (x : Prop) : f (g709 x) = f (g708 x)
@[simp] axiom s709 (x : Prop) : f (g710 x) = f (g709 x)
@[simp] axiom s710 (x : Prop) : f (g711 x) = f (g710 x)
@[simp] axiom s711 (x : Prop) : f (g712 x) = f (g711 x)
@[simp] axiom s712 (x : Prop) : f (g713 x) = f (g712 x)
@[simp] axiom s713 (x : Prop) : f (g714 x) = f (g713 x)
@[simp] axiom s714 (x : Prop) : f (g715 x) = f (g714 x)
@[simp] axiom s715 (x : Prop) : f (g716 x) = f (g715 x)
@[simp] axiom s716 (x : Prop) : f (g717 x) = f (g716 x)
@[simp] axiom s717 (x : Prop) : f (g718 x) = f (g717 x)
@[simp] axiom s718 (x : Prop) : f (g719 x) = f (g718 x)
@[simp] axiom s719 (x : Prop) : f (g720 x) = f (g719 x)
@[simp] axiom s720 (x : Prop) : f (g721 x) = f (g720 x)
@[simp] axiom s721 (x : Prop) : f (g722 x) = f (g721 x)
@[simp] axiom s722 (x : Prop) : f (g723 x) = f (g722 x)
@[simp] axiom s723 (x : Prop) : f (g724 x) = f (g723 x)
@[simp] axiom s724 (x : Prop) : f (g725 x) = f (g724 x)
@[simp] axiom s725 (x : Prop) : f (g726 x) = f (g725 x)
@[simp] axiom s726 (x : Prop) : f (g727 x) = f (g726 x)
@[simp] axiom s727 (x : Prop) : f (g728 x) = f (g727 x)
@[simp] axiom s728 (x : Prop) : f (g729 x) = f (g728 x)
@[simp] axiom s729 (x : Prop) : f (g730 x) = f (g729 x)
@[simp] axiom s730 (x : Prop) : f (g731 x) = f (g730 x)
@[simp] axiom s731 (x : Prop) : f (g732 x) = f (g731 x)
@[simp] axiom s732 (x : Prop) : f (g733 x) = f (g732 x)
@[simp] axiom s733 (x : Prop) : f (g734 x) = f (g733 x)
@[simp] axiom s734 (x : Prop) : f (g735 x) = f (g734 x)
@[simp] axiom s735 (x : Prop) : f (g736 x) = f (g735 x)
@[simp] axiom s736 (x : Prop) : f (g737 x) = f (g736 x)
@[simp] axiom s737 (x : Prop) : f (g738 x) = f (g737 x)
@[simp] axiom s738 (x : Prop) : f (g739 x) = f (g738 x)
@[simp] axiom s739 (x : Prop) : f (g740 x) = f (g739 x)
@[simp] axiom s740 (x : Prop) : f (g741 x) = f (g740 x)
@[simp] axiom s741 (x : Prop) : f (g742 x) = f (g741 x)
@[simp] axiom s742 (x : Prop) : f (g743 x) = f (g742 x)
@[simp] axiom s743 (x : Prop) : f (g744 x) = f (g743 x)
@[simp] axiom s744 (x : Prop) : f (g745 x) = f (g744 x)
@[simp] axiom s745 (x : Prop) : f (g746 x) = f (g745 x)
@[simp] axiom s746 (x : Prop) : f (g747 x) = f (g746 x)
@[simp] axiom s747 (x : Prop) : f (g748 x) = f (g747 x)
@[simp] axiom s748 (x : Prop) : f (g749 x) = f (g748 x)
@[simp] axiom s749 (x : Prop) : f (g750 x) = f (g749 x)
@[simp] axiom s750 (x : Prop) : f (g751 x) = f (g750 x)
@[simp] axiom s751 (x : Prop) : f (g752 x) = f (g751 x)
@[simp] axiom s752 (x : Prop) : f (g753 x) = f (g752 x)
@[simp] axiom s753 (x : Prop) : f (g754 x) = f (g753 x)
@[simp] axiom s754 (x : Prop) : f (g755 x) = f (g754 x)
@[simp] axiom s755 (x : Prop) : f (g756 x) = f (g755 x)
@[simp] axiom s756 (x : Prop) : f (g757 x) = f (g756 x)
@[simp] axiom s757 (x : Prop) : f (g758 x) = f (g757 x)
@[simp] axiom s758 (x : Prop) : f (g759 x) = f (g758 x)
@[simp] axiom s759 (x : Prop) : f (g760 x) = f (g759 x)
@[simp] axiom s760 (x : Prop) : f (g761 x) = f (g760 x)
@[simp] axiom s761 (x : Prop) : f (g762 x) = f (g761 x)
@[simp] axiom s762 (x : Prop) : f (g763 x) = f (g762 x)
@[simp] axiom s763 (x : Prop) : f (g764 x) = f (g763 x)
@[simp] axiom s764 (x : Prop) : f (g765 x) = f (g764 x)
@[simp] axiom s765 (x : Prop) : f (g766 x) = f (g765 x)
@[simp] axiom s766 (x : Prop) : f (g767 x) = f (g766 x)
@[simp] axiom s767 (x : Prop) : f (g768 x) = f (g767 x)
@[simp] axiom s768 (x : Prop) : f (g769 x) = f (g768 x)
@[simp] axiom s769 (x : Prop) : f (g770 x) = f (g769 x)
@[simp] axiom s770 (x : Prop) : f (g771 x) = f (g770 x)
@[simp] axiom s771 (x : Prop) : f (g772 x) = f (g771 x)
@[simp] axiom s772 (x : Prop) : f (g773 x) = f (g772 x)
@[simp] axiom s773 (x : Prop) : f (g774 x) = f (g773 x)
@[simp] axiom s774 (x : Prop) : f (g775 x) = f (g774 x)
@[simp] axiom s775 (x : Prop) : f (g776 x) = f (g775 x)
@[simp] axiom s776 (x : Prop) : f (g777 x) = f (g776 x)
@[simp] axiom s777 (x : Prop) : f (g778 x) = f (g777 x)
@[simp] axiom s778 (x : Prop) : f (g779 x) = f (g778 x)
@[simp] axiom s779 (x : Prop) : f (g780 x) = f (g779 x)
@[simp] axiom s780 (x : Prop) : f (g781 x) = f (g780 x)
@[simp] axiom s781 (x : Prop) : f (g782 x) = f (g781 x)
@[simp] axiom s782 (x : Prop) : f (g783 x) = f (g782 x)
@[simp] axiom s783 (x : Prop) : f (g784 x) = f (g783 x)
@[simp] axiom s784 (x : Prop) : f (g785 x) = f (g784 x)
@[simp] axiom s785 (x : Prop) : f (g786 x) = f (g785 x)
@[simp] axiom s786 (x : Prop) : f (g787 x) = f (g786 x)
@[simp] axiom s787 (x : Prop) : f (g788 x) = f (g787 x)
@[simp] axiom s788 (x : Prop) : f (g789 x) = f (g788 x)
@[simp] axiom s789 (x : Prop) : f (g790 x) = f (g789 x)
@[simp] axiom s790 (x : Prop) : f (g791 x) = f (g790 x)
@[simp] axiom s791 (x : Prop) : f (g792 x) = f (g791 x)
@[simp] axiom s792 (x : Prop) : f (g793 x) = f (g792 x)
@[simp] axiom s793 (x : Prop) : f (g794 x) = f (g793 x)
@[simp] axiom s794 (x : Prop) : f (g795 x) = f (g794 x)
@[simp] axiom s795 (x : Prop) : f (g796 x) = f (g795 x)
@[simp] axiom s796 (x : Prop) : f (g797 x) = f (g796 x)
@[simp] axiom s797 (x : Prop) : f (g798 x) = f (g797 x)
@[simp] axiom s798 (x : Prop) : f (g799 x) = f (g798 x)
@[simp] axiom s799 (x : Prop) : f (g800 x) = f (g799 x)
@[simp] axiom s800 (x : Prop) : f (g801 x) = f (g800 x)
@[simp] axiom s801 (x : Prop) : f (g802 x) = f (g801 x)
@[simp] axiom s802 (x : Prop) : f (g803 x) = f (g802 x)
@[simp] axiom s803 (x : Prop) : f (g804 x) = f (g803 x)
@[simp] axiom s804 (x : Prop) : f (g805 x) = f (g804 x)
@[simp] axiom s805 (x : Prop) : f (g806 x) = f (g805 x)
@[simp] axiom s806 (x : Prop) : f (g807 x) = f (g806 x)
@[simp] axiom s807 (x : Prop) : f (g808 x) = f (g807 x)
@[simp] axiom s808 (x : Prop) : f (g809 x) = f (g808 x)
@[simp] axiom s809 (x : Prop) : f (g810 x) = f (g809 x)
@[simp] axiom s810 (x : Prop) : f (g811 x) = f (g810 x)
@[simp] axiom s811 (x : Prop) : f (g812 x) = f (g811 x)
@[simp] axiom s812 (x : Prop) : f (g813 x) = f (g812 x)
@[simp] axiom s813 (x : Prop) : f (g814 x) = f (g813 x)
@[simp] axiom s814 (x : Prop) : f (g815 x) = f (g814 x)
@[simp] axiom s815 (x : Prop) : f (g816 x) = f (g815 x)
@[simp] axiom s816 (x : Prop) : f (g817 x) = f (g816 x)
@[simp] axiom s817 (x : Prop) : f (g818 x) = f (g817 x)
@[simp] axiom s818 (x : Prop) : f (g819 x) = f (g818 x)
@[simp] axiom s819 (x : Prop) : f (g820 x) = f (g819 x)
@[simp] axiom s820 (x : Prop) : f (g821 x) = f (g820 x)
@[simp] axiom s821 (x : Prop) : f (g822 x) = f (g821 x)
@[simp] axiom s822 (x : Prop) : f (g823 x) = f (g822 x)
@[simp] axiom s823 (x : Prop) : f (g824 x) = f (g823 x)
@[simp] axiom s824 (x : Prop) : f (g825 x) = f (g824 x)
@[simp] axiom s825 (x : Prop) : f (g826 x) = f (g825 x)
@[simp] axiom s826 (x : Prop) : f (g827 x) = f (g826 x)
@[simp] axiom s827 (x : Prop) : f (g828 x) = f (g827 x)
@[simp] axiom s828 (x : Prop) : f (g829 x) = f (g828 x)
@[simp] axiom s829 (x : Prop) : f (g830 x) = f (g829 x)
@[simp] axiom s830 (x : Prop) : f (g831 x) = f (g830 x)
@[simp] axiom s831 (x : Prop) : f (g832 x) = f (g831 x)
@[simp] axiom s832 (x : Prop) : f (g833 x) = f (g832 x)
@[simp] axiom s833 (x : Prop) : f (g834 x) = f (g833 x)
@[simp] axiom s834 (x : Prop) : f (g835 x) = f (g834 x)
@[simp] axiom s835 (x : Prop) : f (g836 x) = f (g835 x)
@[simp] axiom s836 (x : Prop) : f (g837 x) = f (g836 x)
@[simp] axiom s837 (x : Prop) : f (g838 x) = f (g837 x)
@[simp] axiom s838 (x : Prop) : f (g839 x) = f (g838 x)
@[simp] axiom s839 (x : Prop) : f (g840 x) = f (g839 x)
@[simp] axiom s840 (x : Prop) : f (g841 x) = f (g840 x)
@[simp] axiom s841 (x : Prop) : f (g842 x) = f (g841 x)
@[simp] axiom s842 (x : Prop) : f (g843 x) = f (g842 x)
@[simp] axiom s843 (x : Prop) : f (g844 x) = f (g843 x)
@[simp] axiom s844 (x : Prop) : f (g845 x) = f (g844 x)
@[simp] axiom s845 (x : Prop) : f (g846 x) = f (g845 x)
@[simp] axiom s846 (x : Prop) : f (g847 x) = f (g846 x)
@[simp] axiom s847 (x : Prop) : f (g848 x) = f (g847 x)
@[simp] axiom s848 (x : Prop) : f (g849 x) = f (g848 x)
@[simp] axiom s849 (x : Prop) : f (g850 x) = f (g849 x)
@[simp] axiom s850 (x : Prop) : f (g851 x) = f (g850 x)
@[simp] axiom s851 (x : Prop) : f (g852 x) = f (g851 x)
@[simp] axiom s852 (x : Prop) : f (g853 x) = f (g852 x)
@[simp] axiom s853 (x : Prop) : f (g854 x) = f (g853 x)
@[simp] axiom s854 (x : Prop) : f (g855 x) = f (g854 x)
@[simp] axiom s855 (x : Prop) : f (g856 x) = f (g855 x)
@[simp] axiom s856 (x : Prop) : f (g857 x) = f (g856 x)
@[simp] axiom s857 (x : Prop) : f (g858 x) = f (g857 x)
@[simp] axiom s858 (x : Prop) : f (g859 x) = f (g858 x)
@[simp] axiom s859 (x : Prop) : f (g860 x) = f (g859 x)
@[simp] axiom s860 (x : Prop) : f (g861 x) = f (g860 x)
@[simp] axiom s861 (x : Prop) : f (g862 x) = f (g861 x)
@[simp] axiom s862 (x : Prop) : f (g863 x) = f (g862 x)
@[simp] axiom s863 (x : Prop) : f (g864 x) = f (g863 x)
@[simp] axiom s864 (x : Prop) : f (g865 x) = f (g864 x)
@[simp] axiom s865 (x : Prop) : f (g866 x) = f (g865 x)
@[simp] axiom s866 (x : Prop) : f (g867 x) = f (g866 x)
@[simp] axiom s867 (x : Prop) : f (g868 x) = f (g867 x)
@[simp] axiom s868 (x : Prop) : f (g869 x) = f (g868 x)
@[simp] axiom s869 (x : Prop) : f (g870 x) = f (g869 x)
@[simp] axiom s870 (x : Prop) : f (g871 x) = f (g870 x)
@[simp] axiom s871 (x : Prop) : f (g872 x) = f (g871 x)
@[simp] axiom s872 (x : Prop) : f (g873 x) = f (g872 x)
@[simp] axiom s873 (x : Prop) : f (g874 x) = f (g873 x)
@[simp] axiom s874 (x : Prop) : f (g875 x) = f (g874 x)
@[simp] axiom s875 (x : Prop) : f (g876 x) = f (g875 x)
@[simp] axiom s876 (x : Prop) : f (g877 x) = f (g876 x)
@[simp] axiom s877 (x : Prop) : f (g878 x) = f (g877 x)
@[simp] axiom s878 (x : Prop) : f (g879 x) = f (g878 x)
@[simp] axiom s879 (x : Prop) : f (g880 x) = f (g879 x)
@[simp] axiom s880 (x : Prop) : f (g881 x) = f (g880 x)
@[simp] axiom s881 (x : Prop) : f (g882 x) = f (g881 x)
@[simp] axiom s882 (x : Prop) : f (g883 x) = f (g882 x)
@[simp] axiom s883 (x : Prop) : f (g884 x) = f (g883 x)
@[simp] axiom s884 (x : Prop) : f (g885 x) = f (g884 x)
@[simp] axiom s885 (x : Prop) : f (g886 x) = f (g885 x)
@[simp] axiom s886 (x : Prop) : f (g887 x) = f (g886 x)
@[simp] axiom s887 (x : Prop) : f (g888 x) = f (g887 x)
@[simp] axiom s888 (x : Prop) : f (g889 x) = f (g888 x)
@[simp] axiom s889 (x : Prop) : f (g890 x) = f (g889 x)
@[simp] axiom s890 (x : Prop) : f (g891 x) = f (g890 x)
@[simp] axiom s891 (x : Prop) : f (g892 x) = f (g891 x)
@[simp] axiom s892 (x : Prop) : f (g893 x) = f (g892 x)
@[simp] axiom s893 (x : Prop) : f (g894 x) = f (g893 x)
@[simp] axiom s894 (x : Prop) : f (g895 x) = f (g894 x)
@[simp] axiom s895 (x : Prop) : f (g896 x) = f (g895 x)
@[simp] axiom s896 (x : Prop) : f (g897 x) = f (g896 x)
@[simp] axiom s897 (x : Prop) : f (g898 x) = f (g897 x)
@[simp] axiom s898 (x : Prop) : f (g899 x) = f (g898 x)
@[simp] axiom s899 (x : Prop) : f (g900 x) = f (g899 x)
@[simp] axiom s900 (x : Prop) : f (g901 x) = f (g900 x)
@[simp] axiom s901 (x : Prop) : f (g902 x) = f (g901 x)
@[simp] axiom s902 (x : Prop) : f (g903 x) = f (g902 x)
@[simp] axiom s903 (x : Prop) : f (g904 x) = f (g903 x)
@[simp] axiom s904 (x : Prop) : f (g905 x) = f (g904 x)
@[simp] axiom s905 (x : Prop) : f (g906 x) = f (g905 x)
@[simp] axiom s906 (x : Prop) : f (g907 x) = f (g906 x)
@[simp] axiom s907 (x : Prop) : f (g908 x) = f (g907 x)
@[simp] axiom s908 (x : Prop) : f (g909 x) = f (g908 x)
@[simp] axiom s909 (x : Prop) : f (g910 x) = f (g909 x)
@[simp] axiom s910 (x : Prop) : f (g911 x) = f (g910 x)
@[simp] axiom s911 (x : Prop) : f (g912 x) = f (g911 x)
@[simp] axiom s912 (x : Prop) : f (g913 x) = f (g912 x)
@[simp] axiom s913 (x : Prop) : f (g914 x) = f (g913 x)
@[simp] axiom s914 (x : Prop) : f (g915 x) = f (g914 x)
@[simp] axiom s915 (x : Prop) : f (g916 x) = f (g915 x)
@[simp] axiom s916 (x : Prop) : f (g917 x) = f (g916 x)
@[simp] axiom s917 (x : Prop) : f (g918 x) = f (g917 x)
@[simp] axiom s918 (x : Prop) : f (g919 x) = f (g918 x)
@[simp] axiom s919 (x : Prop) : f (g920 x) = f (g919 x)
@[simp] axiom s920 (x : Prop) : f (g921 x) = f (g920 x)
@[simp] axiom s921 (x : Prop) : f (g922 x) = f (g921 x)
@[simp] axiom s922 (x : Prop) : f (g923 x) = f (g922 x)
@[simp] axiom s923 (x : Prop) : f (g924 x) = f (g923 x)
@[simp] axiom s924 (x : Prop) : f (g925 x) = f (g924 x)
@[simp] axiom s925 (x : Prop) : f (g926 x) = f (g925 x)
@[simp] axiom s926 (x : Prop) : f (g927 x) = f (g926 x)
@[simp] axiom s927 (x : Prop) : f (g928 x) = f (g927 x)
@[simp] axiom s928 (x : Prop) : f (g929 x) = f (g928 x)
@[simp] axiom s929 (x : Prop) : f (g930 x) = f (g929 x)
@[simp] axiom s930 (x : Prop) : f (g931 x) = f (g930 x)
@[simp] axiom s931 (x : Prop) : f (g932 x) = f (g931 x)
@[simp] axiom s932 (x : Prop) : f (g933 x) = f (g932 x)
@[simp] axiom s933 (x : Prop) : f (g934 x) = f (g933 x)
@[simp] axiom s934 (x : Prop) : f (g935 x) = f (g934 x)
@[simp] axiom s935 (x : Prop) : f (g936 x) = f (g935 x)
@[simp] axiom s936 (x : Prop) : f (g937 x) = f (g936 x)
@[simp] axiom s937 (x : Prop) : f (g938 x) = f (g937 x)
@[simp] axiom s938 (x : Prop) : f (g939 x) = f (g938 x)
@[simp] axiom s939 (x : Prop) : f (g940 x) = f (g939 x)
@[simp] axiom s940 (x : Prop) : f (g941 x) = f (g940 x)
@[simp] axiom s941 (x : Prop) : f (g942 x) = f (g941 x)
@[simp] axiom s942 (x : Prop) : f (g943 x) = f (g942 x)
@[simp] axiom s943 (x : Prop) : f (g944 x) = f (g943 x)
@[simp] axiom s944 (x : Prop) : f (g945 x) = f (g944 x)
@[simp] axiom s945 (x : Prop) : f (g946 x) = f (g945 x)
@[simp] axiom s946 (x : Prop) : f (g947 x) = f (g946 x)
@[simp] axiom s947 (x : Prop) : f (g948 x) = f (g947 x)
@[simp] axiom s948 (x : Prop) : f (g949 x) = f (g948 x)
@[simp] axiom s949 (x : Prop) : f (g950 x) = f (g949 x)
@[simp] axiom s950 (x : Prop) : f (g951 x) = f (g950 x)
@[simp] axiom s951 (x : Prop) : f (g952 x) = f (g951 x)
@[simp] axiom s952 (x : Prop) : f (g953 x) = f (g952 x)
@[simp] axiom s953 (x : Prop) : f (g954 x) = f (g953 x)
@[simp] axiom s954 (x : Prop) : f (g955 x) = f (g954 x)
@[simp] axiom s955 (x : Prop) : f (g956 x) = f (g955 x)
@[simp] axiom s956 (x : Prop) : f (g957 x) = f (g956 x)
@[simp] axiom s957 (x : Prop) : f (g958 x) = f (g957 x)
@[simp] axiom s958 (x : Prop) : f (g959 x) = f (g958 x)
@[simp] axiom s959 (x : Prop) : f (g960 x) = f (g959 x)
@[simp] axiom s960 (x : Prop) : f (g961 x) = f (g960 x)
@[simp] axiom s961 (x : Prop) : f (g962 x) = f (g961 x)
@[simp] axiom s962 (x : Prop) : f (g963 x) = f (g962 x)
@[simp] axiom s963 (x : Prop) : f (g964 x) = f (g963 x)
@[simp] axiom s964 (x : Prop) : f (g965 x) = f (g964 x)
@[simp] axiom s965 (x : Prop) : f (g966 x) = f (g965 x)
@[simp] axiom s966 (x : Prop) : f (g967 x) = f (g966 x)
@[simp] axiom s967 (x : Prop) : f (g968 x) = f (g967 x)
@[simp] axiom s968 (x : Prop) : f (g969 x) = f (g968 x)
@[simp] axiom s969 (x : Prop) : f (g970 x) = f (g969 x)
@[simp] axiom s970 (x : Prop) : f (g971 x) = f (g970 x)
@[simp] axiom s971 (x : Prop) : f (g972 x) = f (g971 x)
@[simp] axiom s972 (x : Prop) : f (g973 x) = f (g972 x)
@[simp] axiom s973 (x : Prop) : f (g974 x) = f (g973 x)
@[simp] axiom s974 (x : Prop) : f (g975 x) = f (g974 x)
@[simp] axiom s975 (x : Prop) : f (g976 x) = f (g975 x)
@[simp] axiom s976 (x : Prop) : f (g977 x) = f (g976 x)
@[simp] axiom s977 (x : Prop) : f (g978 x) = f (g977 x)
@[simp] axiom s978 (x : Prop) : f (g979 x) = f (g978 x)
@[simp] axiom s979 (x : Prop) : f (g980 x) = f (g979 x)
@[simp] axiom s980 (x : Prop) : f (g981 x) = f (g980 x)
@[simp] axiom s981 (x : Prop) : f (g982 x) = f (g981 x)
@[simp] axiom s982 (x : Prop) : f (g983 x) = f (g982 x)
@[simp] axiom s983 (x : Prop) : f (g984 x) = f (g983 x)
@[simp] axiom s984 (x : Prop) : f (g985 x) = f (g984 x)
@[simp] axiom s985 (x : Prop) : f (g986 x) = f (g985 x)
@[simp] axiom s986 (x : Prop) : f (g987 x) = f (g986 x)
@[simp] axiom s987 (x : Prop) : f (g988 x) = f (g987 x)
@[simp] axiom s988 (x : Prop) : f (g989 x) = f (g988 x)
@[simp] axiom s989 (x : Prop) : f (g990 x) = f (g989 x)
@[simp] axiom s990 (x : Prop) : f (g991 x) = f (g990 x)
@[simp] axiom s991 (x : Prop) : f (g992 x) = f (g991 x)
@[simp] axiom s992 (x : Prop) : f (g993 x) = f (g992 x)
@[simp] axiom s993 (x : Prop) : f (g994 x) = f (g993 x)
@[simp] axiom s994 (x : Prop) : f (g995 x) = f (g994 x)
@[simp] axiom s995 (x : Prop) : f (g996 x) = f (g995 x)
@[simp] axiom s996 (x : Prop) : f (g997 x) = f (g996 x)
@[simp] axiom s997 (x : Prop) : f (g998 x) = f (g997 x)
@[simp] axiom s998 (x : Prop) : f (g999 x) = f (g998 x)
@[simp] axiom s999 (x : Prop) : f (g1000 x) = f (g999 x)
@[simp] axiom s1000 (x : Prop) : f (g1001 x) = f (g1000 x)
@[simp] axiom s1001 (x : Prop) : f (g1002 x) = f (g1001 x)
@[simp] axiom s1002 (x : Prop) : f (g1003 x) = f (g1002 x)
@[simp] axiom s1003 (x : Prop) : f (g1004 x) = f (g1003 x)
@[simp] axiom s1004 (x : Prop) : f (g1005 x) = f (g1004 x)
@[simp] axiom s1005 (x : Prop) : f (g1006 x) = f (g1005 x)
@[simp] axiom s1006 (x : Prop) : f (g1007 x) = f (g1006 x)
@[simp] axiom s1007 (x : Prop) : f (g1008 x) = f (g1007 x)
@[simp] axiom s1008 (x : Prop) : f (g1009 x) = f (g1008 x)
@[simp] axiom s1009 (x : Prop) : f (g1010 x) = f (g1009 x)
@[simp] axiom s1010 (x : Prop) : f (g1011 x) = f (g1010 x)
@[simp] axiom s1011 (x : Prop) : f (g1012 x) = f (g1011 x)
@[simp] axiom s1012 (x : Prop) : f (g1013 x) = f (g1012 x)
@[simp] axiom s1013 (x : Prop) : f (g1014 x) = f (g1013 x)
@[simp] axiom s1014 (x : Prop) : f (g1015 x) = f (g1014 x)
@[simp] axiom s1015 (x : Prop) : f (g1016 x) = f (g1015 x)
@[simp] axiom s1016 (x : Prop) : f (g1017 x) = f (g1016 x)
@[simp] axiom s1017 (x : Prop) : f (g1018 x) = f (g1017 x)
@[simp] axiom s1018 (x : Prop) : f (g1019 x) = f (g1018 x)
@[simp] axiom s1019 (x : Prop) : f (g1020 x) = f (g1019 x)
@[simp] axiom s1020 (x : Prop) : f (g1021 x) = f (g1020 x)
@[simp] axiom s1021 (x : Prop) : f (g1022 x) = f (g1021 x)
@[simp] axiom s1022 (x : Prop) : f (g1023 x) = f (g1022 x)
@[simp] axiom s1023 (x : Prop) : f (g1024 x) = f (g1023 x)
@[simp] axiom s1024 (x : Prop) : f (g1025 x) = f (g1024 x)
@[simp] axiom s1025 (x : Prop) : f (g1026 x) = f (g1025 x)
@[simp] axiom s1026 (x : Prop) : f (g1027 x) = f (g1026 x)
@[simp] axiom s1027 (x : Prop) : f (g1028 x) = f (g1027 x)
@[simp] axiom s1028 (x : Prop) : f (g1029 x) = f (g1028 x)
@[simp] axiom s1029 (x : Prop) : f (g1030 x) = f (g1029 x)
@[simp] axiom s1030 (x : Prop) : f (g1031 x) = f (g1030 x)
@[simp] axiom s1031 (x : Prop) : f (g1032 x) = f (g1031 x)
@[simp] axiom s1032 (x : Prop) : f (g1033 x) = f (g1032 x)
@[simp] axiom s1033 (x : Prop) : f (g1034 x) = f (g1033 x)
@[simp] axiom s1034 (x : Prop) : f (g1035 x) = f (g1034 x)
@[simp] axiom s1035 (x : Prop) : f (g1036 x) = f (g1035 x)
@[simp] axiom s1036 (x : Prop) : f (g1037 x) = f (g1036 x)
@[simp] axiom s1037 (x : Prop) : f (g1038 x) = f (g1037 x)
@[simp] axiom s1038 (x : Prop) : f (g1039 x) = f (g1038 x)
@[simp] axiom s1039 (x : Prop) : f (g1040 x) = f (g1039 x)
@[simp] axiom s1040 (x : Prop) : f (g1041 x) = f (g1040 x)
@[simp] axiom s1041 (x : Prop) : f (g1042 x) = f (g1041 x)
@[simp] axiom s1042 (x : Prop) : f (g1043 x) = f (g1042 x)
@[simp] axiom s1043 (x : Prop) : f (g1044 x) = f (g1043 x)
@[simp] axiom s1044 (x : Prop) : f (g1045 x) = f (g1044 x)
@[simp] axiom s1045 (x : Prop) : f (g1046 x) = f (g1045 x)
@[simp] axiom s1046 (x : Prop) : f (g1047 x) = f (g1046 x)
@[simp] axiom s1047 (x : Prop) : f (g1048 x) = f (g1047 x)
@[simp] axiom s1048 (x : Prop) : f (g1049 x) = f (g1048 x)
@[simp] axiom s1049 (x : Prop) : f (g1050 x) = f (g1049 x)
@[simp] axiom s1050 (x : Prop) : f (g1051 x) = f (g1050 x)
@[simp] axiom s1051 (x : Prop) : f (g1052 x) = f (g1051 x)
@[simp] axiom s1052 (x : Prop) : f (g1053 x) = f (g1052 x)
@[simp] axiom s1053 (x : Prop) : f (g1054 x) = f (g1053 x)
@[simp] axiom s1054 (x : Prop) : f (g1055 x) = f (g1054 x)
@[simp] axiom s1055 (x : Prop) : f (g1056 x) = f (g1055 x)
@[simp] axiom s1056 (x : Prop) : f (g1057 x) = f (g1056 x)
@[simp] axiom s1057 (x : Prop) : f (g1058 x) = f (g1057 x)
@[simp] axiom s1058 (x : Prop) : f (g1059 x) = f (g1058 x)
@[simp] axiom s1059 (x : Prop) : f (g1060 x) = f (g1059 x)
@[simp] axiom s1060 (x : Prop) : f (g1061 x) = f (g1060 x)
@[simp] axiom s1061 (x : Prop) : f (g1062 x) = f (g1061 x)
@[simp] axiom s1062 (x : Prop) : f (g1063 x) = f (g1062 x)
@[simp] axiom s1063 (x : Prop) : f (g1064 x) = f (g1063 x)
@[simp] axiom s1064 (x : Prop) : f (g1065 x) = f (g1064 x)
@[simp] axiom s1065 (x : Prop) : f (g1066 x) = f (g1065 x)
@[simp] axiom s1066 (x : Prop) : f (g1067 x) = f (g1066 x)
@[simp] axiom s1067 (x : Prop) : f (g1068 x) = f (g1067 x)
@[simp] axiom s1068 (x : Prop) : f (g1069 x) = f (g1068 x)
@[simp] axiom s1069 (x : Prop) : f (g1070 x) = f (g1069 x)
@[simp] axiom s1070 (x : Prop) : f (g1071 x) = f (g1070 x)
@[simp] axiom s1071 (x : Prop) : f (g1072 x) = f (g1071 x)
@[simp] axiom s1072 (x : Prop) : f (g1073 x) = f (g1072 x)
@[simp] axiom s1073 (x : Prop) : f (g1074 x) = f (g1073 x)
@[simp] axiom s1074 (x : Prop) : f (g1075 x) = f (g1074 x)
@[simp] axiom s1075 (x : Prop) : f (g1076 x) = f (g1075 x)
@[simp] axiom s1076 (x : Prop) : f (g1077 x) = f (g1076 x)
@[simp] axiom s1077 (x : Prop) : f (g1078 x) = f (g1077 x)
@[simp] axiom s1078 (x : Prop) : f (g1079 x) = f (g1078 x)
@[simp] axiom s1079 (x : Prop) : f (g1080 x) = f (g1079 x)
@[simp] axiom s1080 (x : Prop) : f (g1081 x) = f (g1080 x)
@[simp] axiom s1081 (x : Prop) : f (g1082 x) = f (g1081 x)
@[simp] axiom s1082 (x : Prop) : f (g1083 x) = f (g1082 x)
@[simp] axiom s1083 (x : Prop) : f (g1084 x) = f (g1083 x)
@[simp] axiom s1084 (x : Prop) : f (g1085 x) = f (g1084 x)
@[simp] axiom s1085 (x : Prop) : f (g1086 x) = f (g1085 x)
@[simp] axiom s1086 (x : Prop) : f (g1087 x) = f (g1086 x)
@[simp] axiom s1087 (x : Prop) : f (g1088 x) = f (g1087 x)
@[simp] axiom s1088 (x : Prop) : f (g1089 x) = f (g1088 x)
@[simp] axiom s1089 (x : Prop) : f (g1090 x) = f (g1089 x)
@[simp] axiom s1090 (x : Prop) : f (g1091 x) = f (g1090 x)
@[simp] axiom s1091 (x : Prop) : f (g1092 x) = f (g1091 x)
@[simp] axiom s1092 (x : Prop) : f (g1093 x) = f (g1092 x)
@[simp] axiom s1093 (x : Prop) : f (g1094 x) = f (g1093 x)
@[simp] axiom s1094 (x : Prop) : f (g1095 x) = f (g1094 x)
@[simp] axiom s1095 (x : Prop) : f (g1096 x) = f (g1095 x)
@[simp] axiom s1096 (x : Prop) : f (g1097 x) = f (g1096 x)
@[simp] axiom s1097 (x : Prop) : f (g1098 x) = f (g1097 x)
@[simp] axiom s1098 (x : Prop) : f (g1099 x) = f (g1098 x)
@[simp] axiom s1099 (x : Prop) : f (g1100 x) = f (g1099 x)
@[simp] axiom s1100 (x : Prop) : f (g1101 x) = f (g1100 x)
@[simp] axiom s1101 (x : Prop) : f (g1102 x) = f (g1101 x)
@[simp] axiom s1102 (x : Prop) : f (g1103 x) = f (g1102 x)
@[simp] axiom s1103 (x : Prop) : f (g1104 x) = f (g1103 x)
@[simp] axiom s1104 (x : Prop) : f (g1105 x) = f (g1104 x)
@[simp] axiom s1105 (x : Prop) : f (g1106 x) = f (g1105 x)
@[simp] axiom s1106 (x : Prop) : f (g1107 x) = f (g1106 x)
@[simp] axiom s1107 (x : Prop) : f (g1108 x) = f (g1107 x)
@[simp] axiom s1108 (x : Prop) : f (g1109 x) = f (g1108 x)
@[simp] axiom s1109 (x : Prop) : f (g1110 x) = f (g1109 x)
@[simp] axiom s1110 (x : Prop) : f (g1111 x) = f (g1110 x)
@[simp] axiom s1111 (x : Prop) : f (g1112 x) = f (g1111 x)
@[simp] axiom s1112 (x : Prop) : f (g1113 x) = f (g1112 x)
@[simp] axiom s1113 (x : Prop) : f (g1114 x) = f (g1113 x)
@[simp] axiom s1114 (x : Prop) : f (g1115 x) = f (g1114 x)
@[simp] axiom s1115 (x : Prop) : f (g1116 x) = f (g1115 x)
@[simp] axiom s1116 (x : Prop) : f (g1117 x) = f (g1116 x)
@[simp] axiom s1117 (x : Prop) : f (g1118 x) = f (g1117 x)
@[simp] axiom s1118 (x : Prop) : f (g1119 x) = f (g1118 x)
@[simp] axiom s1119 (x : Prop) : f (g1120 x) = f (g1119 x)
@[simp] axiom s1120 (x : Prop) : f (g1121 x) = f (g1120 x)
@[simp] axiom s1121 (x : Prop) : f (g1122 x) = f (g1121 x)
@[simp] axiom s1122 (x : Prop) : f (g1123 x) = f (g1122 x)
@[simp] axiom s1123 (x : Prop) : f (g1124 x) = f (g1123 x)
@[simp] axiom s1124 (x : Prop) : f (g1125 x) = f (g1124 x)
@[simp] axiom s1125 (x : Prop) : f (g1126 x) = f (g1125 x)
@[simp] axiom s1126 (x : Prop) : f (g1127 x) = f (g1126 x)
@[simp] axiom s1127 (x : Prop) : f (g1128 x) = f (g1127 x)
@[simp] axiom s1128 (x : Prop) : f (g1129 x) = f (g1128 x)
@[simp] axiom s1129 (x : Prop) : f (g1130 x) = f (g1129 x)
@[simp] axiom s1130 (x : Prop) : f (g1131 x) = f (g1130 x)
@[simp] axiom s1131 (x : Prop) : f (g1132 x) = f (g1131 x)
@[simp] axiom s1132 (x : Prop) : f (g1133 x) = f (g1132 x)
@[simp] axiom s1133 (x : Prop) : f (g1134 x) = f (g1133 x)
@[simp] axiom s1134 (x : Prop) : f (g1135 x) = f (g1134 x)
@[simp] axiom s1135 (x : Prop) : f (g1136 x) = f (g1135 x)
@[simp] axiom s1136 (x : Prop) : f (g1137 x) = f (g1136 x)
@[simp] axiom s1137 (x : Prop) : f (g1138 x) = f (g1137 x)
@[simp] axiom s1138 (x : Prop) : f (g1139 x) = f (g1138 x)
@[simp] axiom s1139 (x : Prop) : f (g1140 x) = f (g1139 x)
@[simp] axiom s1140 (x : Prop) : f (g1141 x) = f (g1140 x)
@[simp] axiom s1141 (x : Prop) : f (g1142 x) = f (g1141 x)
@[simp] axiom s1142 (x : Prop) : f (g1143 x) = f (g1142 x)
@[simp] axiom s1143 (x : Prop) : f (g1144 x) = f (g1143 x)
@[simp] axiom s1144 (x : Prop) : f (g1145 x) = f (g1144 x)
@[simp] axiom s1145 (x : Prop) : f (g1146 x) = f (g1145 x)
@[simp] axiom s1146 (x : Prop) : f (g1147 x) = f (g1146 x)
@[simp] axiom s1147 (x : Prop) : f (g1148 x) = f (g1147 x)
@[simp] axiom s1148 (x : Prop) : f (g1149 x) = f (g1148 x)
@[simp] axiom s1149 (x : Prop) : f (g1150 x) = f (g1149 x)
@[simp] axiom s1150 (x : Prop) : f (g1151 x) = f (g1150 x)
@[simp] axiom s1151 (x : Prop) : f (g1152 x) = f (g1151 x)
@[simp] axiom s1152 (x : Prop) : f (g1153 x) = f (g1152 x)
@[simp] axiom s1153 (x : Prop) : f (g1154 x) = f (g1153 x)
@[simp] axiom s1154 (x : Prop) : f (g1155 x) = f (g1154 x)
@[simp] axiom s1155 (x : Prop) : f (g1156 x) = f (g1155 x)
@[simp] axiom s1156 (x : Prop) : f (g1157 x) = f (g1156 x)
@[simp] axiom s1157 (x : Prop) : f (g1158 x) = f (g1157 x)
@[simp] axiom s1158 (x : Prop) : f (g1159 x) = f (g1158 x)
@[simp] axiom s1159 (x : Prop) : f (g1160 x) = f (g1159 x)
@[simp] axiom s1160 (x : Prop) : f (g1161 x) = f (g1160 x)
@[simp] axiom s1161 (x : Prop) : f (g1162 x) = f (g1161 x)
@[simp] axiom s1162 (x : Prop) : f (g1163 x) = f (g1162 x)
@[simp] axiom s1163 (x : Prop) : f (g1164 x) = f (g1163 x)
@[simp] axiom s1164 (x : Prop) : f (g1165 x) = f (g1164 x)
@[simp] axiom s1165 (x : Prop) : f (g1166 x) = f (g1165 x)
@[simp] axiom s1166 (x : Prop) : f (g1167 x) = f (g1166 x)
@[simp] axiom s1167 (x : Prop) : f (g1168 x) = f (g1167 x)
@[simp] axiom s1168 (x : Prop) : f (g1169 x) = f (g1168 x)
@[simp] axiom s1169 (x : Prop) : f (g1170 x) = f (g1169 x)
@[simp] axiom s1170 (x : Prop) : f (g1171 x) = f (g1170 x)
@[simp] axiom s1171 (x : Prop) : f (g1172 x) = f (g1171 x)
@[simp] axiom s1172 (x : Prop) : f (g1173 x) = f (g1172 x)
@[simp] axiom s1173 (x : Prop) : f (g1174 x) = f (g1173 x)
@[simp] axiom s1174 (x : Prop) : f (g1175 x) = f (g1174 x)
@[simp] axiom s1175 (x : Prop) : f (g1176 x) = f (g1175 x)
@[simp] axiom s1176 (x : Prop) : f (g1177 x) = f (g1176 x)
@[simp] axiom s1177 (x : Prop) : f (g1178 x) = f (g1177 x)
@[simp] axiom s1178 (x : Prop) : f (g1179 x) = f (g1178 x)
@[simp] axiom s1179 (x : Prop) : f (g1180 x) = f (g1179 x)
@[simp] axiom s1180 (x : Prop) : f (g1181 x) = f (g1180 x)
@[simp] axiom s1181 (x : Prop) : f (g1182 x) = f (g1181 x)
@[simp] axiom s1182 (x : Prop) : f (g1183 x) = f (g1182 x)
@[simp] axiom s1183 (x : Prop) : f (g1184 x) = f (g1183 x)
@[simp] axiom s1184 (x : Prop) : f (g1185 x) = f (g1184 x)
@[simp] axiom s1185 (x : Prop) : f (g1186 x) = f (g1185 x)
@[simp] axiom s1186 (x : Prop) : f (g1187 x) = f (g1186 x)
@[simp] axiom s1187 (x : Prop) : f (g1188 x) = f (g1187 x)
@[simp] axiom s1188 (x : Prop) : f (g1189 x) = f (g1188 x)
@[simp] axiom s1189 (x : Prop) : f (g1190 x) = f (g1189 x)
@[simp] axiom s1190 (x : Prop) : f (g1191 x) = f (g1190 x)
@[simp] axiom s1191 (x : Prop) : f (g1192 x) = f (g1191 x)
@[simp] axiom s1192 (x : Prop) : f (g1193 x) = f (g1192 x)
@[simp] axiom s1193 (x : Prop) : f (g1194 x) = f (g1193 x)
@[simp] axiom s1194 (x : Prop) : f (g1195 x) = f (g1194 x)
@[simp] axiom s1195 (x : Prop) : f (g1196 x) = f (g1195 x)
@[simp] axiom s1196 (x : Prop) : f (g1197 x) = f (g1196 x)
@[simp] axiom s1197 (x : Prop) : f (g1198 x) = f (g1197 x)
@[simp] axiom s1198 (x : Prop) : f (g1199 x) = f (g1198 x)
@[simp] axiom s1199 (x : Prop) : f (g1200 x) = f (g1199 x)
@[simp] axiom s1200 (x : Prop) : f (g1201 x) = f (g1200 x)
@[simp] axiom s1201 (x : Prop) : f (g1202 x) = f (g1201 x)
@[simp] axiom s1202 (x : Prop) : f (g1203 x) = f (g1202 x)
@[simp] axiom s1203 (x : Prop) : f (g1204 x) = f (g1203 x)
@[simp] axiom s1204 (x : Prop) : f (g1205 x) = f (g1204 x)
@[simp] axiom s1205 (x : Prop) : f (g1206 x) = f (g1205 x)
@[simp] axiom s1206 (x : Prop) : f (g1207 x) = f (g1206 x)
@[simp] axiom s1207 (x : Prop) : f (g1208 x) = f (g1207 x)
@[simp] axiom s1208 (x : Prop) : f (g1209 x) = f (g1208 x)
@[simp] axiom s1209 (x : Prop) : f (g1210 x) = f (g1209 x)
@[simp] axiom s1210 (x : Prop) : f (g1211 x) = f (g1210 x)
@[simp] axiom s1211 (x : Prop) : f (g1212 x) = f (g1211 x)
@[simp] axiom s1212 (x : Prop) : f (g1213 x) = f (g1212 x)
@[simp] axiom s1213 (x : Prop) : f (g1214 x) = f (g1213 x)
@[simp] axiom s1214 (x : Prop) : f (g1215 x) = f (g1214 x)
@[simp] axiom s1215 (x : Prop) : f (g1216 x) = f (g1215 x)
@[simp] axiom s1216 (x : Prop) : f (g1217 x) = f (g1216 x)
@[simp] axiom s1217 (x : Prop) : f (g1218 x) = f (g1217 x)
@[simp] axiom s1218 (x : Prop) : f (g1219 x) = f (g1218 x)
@[simp] axiom s1219 (x : Prop) : f (g1220 x) = f (g1219 x)
@[simp] axiom s1220 (x : Prop) : f (g1221 x) = f (g1220 x)
@[simp] axiom s1221 (x : Prop) : f (g1222 x) = f (g1221 x)
@[simp] axiom s1222 (x : Prop) : f (g1223 x) = f (g1222 x)
@[simp] axiom s1223 (x : Prop) : f (g1224 x) = f (g1223 x)
@[simp] axiom s1224 (x : Prop) : f (g1225 x) = f (g1224 x)
@[simp] axiom s1225 (x : Prop) : f (g1226 x) = f (g1225 x)
@[simp] axiom s1226 (x : Prop) : f (g1227 x) = f (g1226 x)
@[simp] axiom s1227 (x : Prop) : f (g1228 x) = f (g1227 x)
@[simp] axiom s1228 (x : Prop) : f (g1229 x) = f (g1228 x)
@[simp] axiom s1229 (x : Prop) : f (g1230 x) = f (g1229 x)
@[simp] axiom s1230 (x : Prop) : f (g1231 x) = f (g1230 x)
@[simp] axiom s1231 (x : Prop) : f (g1232 x) = f (g1231 x)
@[simp] axiom s1232 (x : Prop) : f (g1233 x) = f (g1232 x)
@[simp] axiom s1233 (x : Prop) : f (g1234 x) = f (g1233 x)
@[simp] axiom s1234 (x : Prop) : f (g1235 x) = f (g1234 x)
@[simp] axiom s1235 (x : Prop) : f (g1236 x) = f (g1235 x)
@[simp] axiom s1236 (x : Prop) : f (g1237 x) = f (g1236 x)
@[simp] axiom s1237 (x : Prop) : f (g1238 x) = f (g1237 x)
@[simp] axiom s1238 (x : Prop) : f (g1239 x) = f (g1238 x)
@[simp] axiom s1239 (x : Prop) : f (g1240 x) = f (g1239 x)
@[simp] axiom s1240 (x : Prop) : f (g1241 x) = f (g1240 x)
@[simp] axiom s1241 (x : Prop) : f (g1242 x) = f (g1241 x)
@[simp] axiom s1242 (x : Prop) : f (g1243 x) = f (g1242 x)
@[simp] axiom s1243 (x : Prop) : f (g1244 x) = f (g1243 x)
@[simp] axiom s1244 (x : Prop) : f (g1245 x) = f (g1244 x)
@[simp] axiom s1245 (x : Prop) : f (g1246 x) = f (g1245 x)
@[simp] axiom s1246 (x : Prop) : f (g1247 x) = f (g1246 x)
@[simp] axiom s1247 (x : Prop) : f (g1248 x) = f (g1247 x)
@[simp] axiom s1248 (x : Prop) : f (g1249 x) = f (g1248 x)
@[simp] axiom s1249 (x : Prop) : f (g1250 x) = f (g1249 x)
@[simp] axiom s1250 (x : Prop) : f (g1251 x) = f (g1250 x)
@[simp] axiom s1251 (x : Prop) : f (g1252 x) = f (g1251 x)
@[simp] axiom s1252 (x : Prop) : f (g1253 x) = f (g1252 x)
@[simp] axiom s1253 (x : Prop) : f (g1254 x) = f (g1253 x)
@[simp] axiom s1254 (x : Prop) : f (g1255 x) = f (g1254 x)
@[simp] axiom s1255 (x : Prop) : f (g1256 x) = f (g1255 x)
@[simp] axiom s1256 (x : Prop) : f (g1257 x) = f (g1256 x)
@[simp] axiom s1257 (x : Prop) : f (g1258 x) = f (g1257 x)
@[simp] axiom s1258 (x : Prop) : f (g1259 x) = f (g1258 x)
@[simp] axiom s1259 (x : Prop) : f (g1260 x) = f (g1259 x)
@[simp] axiom s1260 (x : Prop) : f (g1261 x) = f (g1260 x)
@[simp] axiom s1261 (x : Prop) : f (g1262 x) = f (g1261 x)
@[simp] axiom s1262 (x : Prop) : f (g1263 x) = f (g1262 x)
@[simp] axiom s1263 (x : Prop) : f (g1264 x) = f (g1263 x)
@[simp] axiom s1264 (x : Prop) : f (g1265 x) = f (g1264 x)
@[simp] axiom s1265 (x : Prop) : f (g1266 x) = f (g1265 x)
@[simp] axiom s1266 (x : Prop) : f (g1267 x) = f (g1266 x)
@[simp] axiom s1267 (x : Prop) : f (g1268 x) = f (g1267 x)
@[simp] axiom s1268 (x : Prop) : f (g1269 x) = f (g1268 x)
@[simp] axiom s1269 (x : Prop) : f (g1270 x) = f (g1269 x)
@[simp] axiom s1270 (x : Prop) : f (g1271 x) = f (g1270 x)
@[simp] axiom s1271 (x : Prop) : f (g1272 x) = f (g1271 x)
@[simp] axiom s1272 (x : Prop) : f (g1273 x) = f (g1272 x)
@[simp] axiom s1273 (x : Prop) : f (g1274 x) = f (g1273 x)
@[simp] axiom s1274 (x : Prop) : f (g1275 x) = f (g1274 x)
@[simp] axiom s1275 (x : Prop) : f (g1276 x) = f (g1275 x)
@[simp] axiom s1276 (x : Prop) : f (g1277 x) = f (g1276 x)
@[simp] axiom s1277 (x : Prop) : f (g1278 x) = f (g1277 x)
@[simp] axiom s1278 (x : Prop) : f (g1279 x) = f (g1278 x)
@[simp] axiom s1279 (x : Prop) : f (g1280 x) = f (g1279 x)
@[simp] axiom s1280 (x : Prop) : f (g1281 x) = f (g1280 x)
@[simp] axiom s1281 (x : Prop) : f (g1282 x) = f (g1281 x)
@[simp] axiom s1282 (x : Prop) : f (g1283 x) = f (g1282 x)
@[simp] axiom s1283 (x : Prop) : f (g1284 x) = f (g1283 x)
@[simp] axiom s1284 (x : Prop) : f (g1285 x) = f (g1284 x)
@[simp] axiom s1285 (x : Prop) : f (g1286 x) = f (g1285 x)
@[simp] axiom s1286 (x : Prop) : f (g1287 x) = f (g1286 x)
@[simp] axiom s1287 (x : Prop) : f (g1288 x) = f (g1287 x)
@[simp] axiom s1288 (x : Prop) : f (g1289 x) = f (g1288 x)
@[simp] axiom s1289 (x : Prop) : f (g1290 x) = f (g1289 x)
@[simp] axiom s1290 (x : Prop) : f (g1291 x) = f (g1290 x)
@[simp] axiom s1291 (x : Prop) : f (g1292 x) = f (g1291 x)
@[simp] axiom s1292 (x : Prop) : f (g1293 x) = f (g1292 x)
@[simp] axiom s1293 (x : Prop) : f (g1294 x) = f (g1293 x)
@[simp] axiom s1294 (x : Prop) : f (g1295 x) = f (g1294 x)
@[simp] axiom s1295 (x : Prop) : f (g1296 x) = f (g1295 x)
@[simp] axiom s1296 (x : Prop) : f (g1297 x) = f (g1296 x)
@[simp] axiom s1297 (x : Prop) : f (g1298 x) = f (g1297 x)
@[simp] axiom s1298 (x : Prop) : f (g1299 x) = f (g1298 x)
@[simp] axiom s1299 (x : Prop) : f (g1300 x) = f (g1299 x)
@[simp] axiom s1300 (x : Prop) : f (g1301 x) = f (g1300 x)
@[simp] axiom s1301 (x : Prop) : f (g1302 x) = f (g1301 x)
@[simp] axiom s1302 (x : Prop) : f (g1303 x) = f (g1302 x)
@[simp] axiom s1303 (x : Prop) : f (g1304 x) = f (g1303 x)
@[simp] axiom s1304 (x : Prop) : f (g1305 x) = f (g1304 x)
@[simp] axiom s1305 (x : Prop) : f (g1306 x) = f (g1305 x)
@[simp] axiom s1306 (x : Prop) : f (g1307 x) = f (g1306 x)
@[simp] axiom s1307 (x : Prop) : f (g1308 x) = f (g1307 x)
@[simp] axiom s1308 (x : Prop) : f (g1309 x) = f (g1308 x)
@[simp] axiom s1309 (x : Prop) : f (g1310 x) = f (g1309 x)
@[simp] axiom s1310 (x : Prop) : f (g1311 x) = f (g1310 x)
@[simp] axiom s1311 (x : Prop) : f (g1312 x) = f (g1311 x)
@[simp] axiom s1312 (x : Prop) : f (g1313 x) = f (g1312 x)
@[simp] axiom s1313 (x : Prop) : f (g1314 x) = f (g1313 x)
@[simp] axiom s1314 (x : Prop) : f (g1315 x) = f (g1314 x)
@[simp] axiom s1315 (x : Prop) : f (g1316 x) = f (g1315 x)
@[simp] axiom s1316 (x : Prop) : f (g1317 x) = f (g1316 x)
@[simp] axiom s1317 (x : Prop) : f (g1318 x) = f (g1317 x)
@[simp] axiom s1318 (x : Prop) : f (g1319 x) = f (g1318 x)
@[simp] axiom s1319 (x : Prop) : f (g1320 x) = f (g1319 x)
@[simp] axiom s1320 (x : Prop) : f (g1321 x) = f (g1320 x)
@[simp] axiom s1321 (x : Prop) : f (g1322 x) = f (g1321 x)
@[simp] axiom s1322 (x : Prop) : f (g1323 x) = f (g1322 x)
@[simp] axiom s1323 (x : Prop) : f (g1324 x) = f (g1323 x)
@[simp] axiom s1324 (x : Prop) : f (g1325 x) = f (g1324 x)
@[simp] axiom s1325 (x : Prop) : f (g1326 x) = f (g1325 x)
@[simp] axiom s1326 (x : Prop) : f (g1327 x) = f (g1326 x)
@[simp] axiom s1327 (x : Prop) : f (g1328 x) = f (g1327 x)
@[simp] axiom s1328 (x : Prop) : f (g1329 x) = f (g1328 x)
@[simp] axiom s1329 (x : Prop) : f (g1330 x) = f (g1329 x)
@[simp] axiom s1330 (x : Prop) : f (g1331 x) = f (g1330 x)
@[simp] axiom s1331 (x : Prop) : f (g1332 x) = f (g1331 x)
@[simp] axiom s1332 (x : Prop) : f (g1333 x) = f (g1332 x)
@[simp] axiom s1333 (x : Prop) : f (g1334 x) = f (g1333 x)
@[simp] axiom s1334 (x : Prop) : f (g1335 x) = f (g1334 x)
@[simp] axiom s1335 (x : Prop) : f (g1336 x) = f (g1335 x)
@[simp] axiom s1336 (x : Prop) : f (g1337 x) = f (g1336 x)
@[simp] axiom s1337 (x : Prop) : f (g1338 x) = f (g1337 x)
@[simp] axiom s1338 (x : Prop) : f (g1339 x) = f (g1338 x)
@[simp] axiom s1339 (x : Prop) : f (g1340 x) = f (g1339 x)
@[simp] axiom s1340 (x : Prop) : f (g1341 x) = f (g1340 x)
@[simp] axiom s1341 (x : Prop) : f (g1342 x) = f (g1341 x)
@[simp] axiom s1342 (x : Prop) : f (g1343 x) = f (g1342 x)
@[simp] axiom s1343 (x : Prop) : f (g1344 x) = f (g1343 x)
@[simp] axiom s1344 (x : Prop) : f (g1345 x) = f (g1344 x)
@[simp] axiom s1345 (x : Prop) : f (g1346 x) = f (g1345 x)
@[simp] axiom s1346 (x : Prop) : f (g1347 x) = f (g1346 x)
@[simp] axiom s1347 (x : Prop) : f (g1348 x) = f (g1347 x)
@[simp] axiom s1348 (x : Prop) : f (g1349 x) = f (g1348 x)
@[simp] axiom s1349 (x : Prop) : f (g1350 x) = f (g1349 x)
@[simp] axiom s1350 (x : Prop) : f (g1351 x) = f (g1350 x)
@[simp] axiom s1351 (x : Prop) : f (g1352 x) = f (g1351 x)
@[simp] axiom s1352 (x : Prop) : f (g1353 x) = f (g1352 x)
@[simp] axiom s1353 (x : Prop) : f (g1354 x) = f (g1353 x)
@[simp] axiom s1354 (x : Prop) : f (g1355 x) = f (g1354 x)
@[simp] axiom s1355 (x : Prop) : f (g1356 x) = f (g1355 x)
@[simp] axiom s1356 (x : Prop) : f (g1357 x) = f (g1356 x)
@[simp] axiom s1357 (x : Prop) : f (g1358 x) = f (g1357 x)
@[simp] axiom s1358 (x : Prop) : f (g1359 x) = f (g1358 x)
@[simp] axiom s1359 (x : Prop) : f (g1360 x) = f (g1359 x)
@[simp] axiom s1360 (x : Prop) : f (g1361 x) = f (g1360 x)
@[simp] axiom s1361 (x : Prop) : f (g1362 x) = f (g1361 x)
@[simp] axiom s1362 (x : Prop) : f (g1363 x) = f (g1362 x)
@[simp] axiom s1363 (x : Prop) : f (g1364 x) = f (g1363 x)
@[simp] axiom s1364 (x : Prop) : f (g1365 x) = f (g1364 x)
@[simp] axiom s1365 (x : Prop) : f (g1366 x) = f (g1365 x)
@[simp] axiom s1366 (x : Prop) : f (g1367 x) = f (g1366 x)
@[simp] axiom s1367 (x : Prop) : f (g1368 x) = f (g1367 x)
@[simp] axiom s1368 (x : Prop) : f (g1369 x) = f (g1368 x)
@[simp] axiom s1369 (x : Prop) : f (g1370 x) = f (g1369 x)
@[simp] axiom s1370 (x : Prop) : f (g1371 x) = f (g1370 x)
@[simp] axiom s1371 (x : Prop) : f (g1372 x) = f (g1371 x)
@[simp] axiom s1372 (x : Prop) : f (g1373 x) = f (g1372 x)
@[simp] axiom s1373 (x : Prop) : f (g1374 x) = f (g1373 x)
@[simp] axiom s1374 (x : Prop) : f (g1375 x) = f (g1374 x)
@[simp] axiom s1375 (x : Prop) : f (g1376 x) = f (g1375 x)
@[simp] axiom s1376 (x : Prop) : f (g1377 x) = f (g1376 x)
@[simp] axiom s1377 (x : Prop) : f (g1378 x) = f (g1377 x)
@[simp] axiom s1378 (x : Prop) : f (g1379 x) = f (g1378 x)
@[simp] axiom s1379 (x : Prop) : f (g1380 x) = f (g1379 x)
@[simp] axiom s1380 (x : Prop) : f (g1381 x) = f (g1380 x)
@[simp] axiom s1381 (x : Prop) : f (g1382 x) = f (g1381 x)
@[simp] axiom s1382 (x : Prop) : f (g1383 x) = f (g1382 x)
@[simp] axiom s1383 (x : Prop) : f (g1384 x) = f (g1383 x)
@[simp] axiom s1384 (x : Prop) : f (g1385 x) = f (g1384 x)
@[simp] axiom s1385 (x : Prop) : f (g1386 x) = f (g1385 x)
@[simp] axiom s1386 (x : Prop) : f (g1387 x) = f (g1386 x)
@[simp] axiom s1387 (x : Prop) : f (g1388 x) = f (g1387 x)
@[simp] axiom s1388 (x : Prop) : f (g1389 x) = f (g1388 x)
@[simp] axiom s1389 (x : Prop) : f (g1390 x) = f (g1389 x)
@[simp] axiom s1390 (x : Prop) : f (g1391 x) = f (g1390 x)
@[simp] axiom s1391 (x : Prop) : f (g1392 x) = f (g1391 x)
@[simp] axiom s1392 (x : Prop) : f (g1393 x) = f (g1392 x)
@[simp] axiom s1393 (x : Prop) : f (g1394 x) = f (g1393 x)
@[simp] axiom s1394 (x : Prop) : f (g1395 x) = f (g1394 x)
@[simp] axiom s1395 (x : Prop) : f (g1396 x) = f (g1395 x)
@[simp] axiom s1396 (x : Prop) : f (g1397 x) = f (g1396 x)
@[simp] axiom s1397 (x : Prop) : f (g1398 x) = f (g1397 x)
@[simp] axiom s1398 (x : Prop) : f (g1399 x) = f (g1398 x)
@[simp] axiom s1399 (x : Prop) : f (g1400 x) = f (g1399 x)
@[simp] axiom s1400 (x : Prop) : f (g1401 x) = f (g1400 x)
@[simp] axiom s1401 (x : Prop) : f (g1402 x) = f (g1401 x)
@[simp] axiom s1402 (x : Prop) : f (g1403 x) = f (g1402 x)
@[simp] axiom s1403 (x : Prop) : f (g1404 x) = f (g1403 x)
@[simp] axiom s1404 (x : Prop) : f (g1405 x) = f (g1404 x)
@[simp] axiom s1405 (x : Prop) : f (g1406 x) = f (g1405 x)
@[simp] axiom s1406 (x : Prop) : f (g1407 x) = f (g1406 x)
@[simp] axiom s1407 (x : Prop) : f (g1408 x) = f (g1407 x)
@[simp] axiom s1408 (x : Prop) : f (g1409 x) = f (g1408 x)
@[simp] axiom s1409 (x : Prop) : f (g1410 x) = f (g1409 x)
@[simp] axiom s1410 (x : Prop) : f (g1411 x) = f (g1410 x)
@[simp] axiom s1411 (x : Prop) : f (g1412 x) = f (g1411 x)
@[simp] axiom s1412 (x : Prop) : f (g1413 x) = f (g1412 x)
@[simp] axiom s1413 (x : Prop) : f (g1414 x) = f (g1413 x)
@[simp] axiom s1414 (x : Prop) : f (g1415 x) = f (g1414 x)
@[simp] axiom s1415 (x : Prop) : f (g1416 x) = f (g1415 x)
@[simp] axiom s1416 (x : Prop) : f (g1417 x) = f (g1416 x)
@[simp] axiom s1417 (x : Prop) : f (g1418 x) = f (g1417 x)
@[simp] axiom s1418 (x : Prop) : f (g1419 x) = f (g1418 x)
@[simp] axiom s1419 (x : Prop) : f (g1420 x) = f (g1419 x)
@[simp] axiom s1420 (x : Prop) : f (g1421 x) = f (g1420 x)
@[simp] axiom s1421 (x : Prop) : f (g1422 x) = f (g1421 x)
@[simp] axiom s1422 (x : Prop) : f (g1423 x) = f (g1422 x)
@[simp] axiom s1423 (x : Prop) : f (g1424 x) = f (g1423 x)
@[simp] axiom s1424 (x : Prop) : f (g1425 x) = f (g1424 x)
@[simp] axiom s1425 (x : Prop) : f (g1426 x) = f (g1425 x)
@[simp] axiom s1426 (x : Prop) : f (g1427 x) = f (g1426 x)
@[simp] axiom s1427 (x : Prop) : f (g1428 x) = f (g1427 x)
@[simp] axiom s1428 (x : Prop) : f (g1429 x) = f (g1428 x)
@[simp] axiom s1429 (x : Prop) : f (g1430 x) = f (g1429 x)
@[simp] axiom s1430 (x : Prop) : f (g1431 x) = f (g1430 x)
@[simp] axiom s1431 (x : Prop) : f (g1432 x) = f (g1431 x)
@[simp] axiom s1432 (x : Prop) : f (g1433 x) = f (g1432 x)
@[simp] axiom s1433 (x : Prop) : f (g1434 x) = f (g1433 x)
@[simp] axiom s1434 (x : Prop) : f (g1435 x) = f (g1434 x)
@[simp] axiom s1435 (x : Prop) : f (g1436 x) = f (g1435 x)
@[simp] axiom s1436 (x : Prop) : f (g1437 x) = f (g1436 x)
@[simp] axiom s1437 (x : Prop) : f (g1438 x) = f (g1437 x)
@[simp] axiom s1438 (x : Prop) : f (g1439 x) = f (g1438 x)
@[simp] axiom s1439 (x : Prop) : f (g1440 x) = f (g1439 x)
@[simp] axiom s1440 (x : Prop) : f (g1441 x) = f (g1440 x)
@[simp] axiom s1441 (x : Prop) : f (g1442 x) = f (g1441 x)
@[simp] axiom s1442 (x : Prop) : f (g1443 x) = f (g1442 x)
@[simp] axiom s1443 (x : Prop) : f (g1444 x) = f (g1443 x)
@[simp] axiom s1444 (x : Prop) : f (g1445 x) = f (g1444 x)
@[simp] axiom s1445 (x : Prop) : f (g1446 x) = f (g1445 x)
@[simp] axiom s1446 (x : Prop) : f (g1447 x) = f (g1446 x)
@[simp] axiom s1447 (x : Prop) : f (g1448 x) = f (g1447 x)
@[simp] axiom s1448 (x : Prop) : f (g1449 x) = f (g1448 x)
@[simp] axiom s1449 (x : Prop) : f (g1450 x) = f (g1449 x)
@[simp] axiom s1450 (x : Prop) : f (g1451 x) = f (g1450 x)
@[simp] axiom s1451 (x : Prop) : f (g1452 x) = f (g1451 x)
@[simp] axiom s1452 (x : Prop) : f (g1453 x) = f (g1452 x)
@[simp] axiom s1453 (x : Prop) : f (g1454 x) = f (g1453 x)
@[simp] axiom s1454 (x : Prop) : f (g1455 x) = f (g1454 x)
@[simp] axiom s1455 (x : Prop) : f (g1456 x) = f (g1455 x)
@[simp] axiom s1456 (x : Prop) : f (g1457 x) = f (g1456 x)
@[simp] axiom s1457 (x : Prop) : f (g1458 x) = f (g1457 x)
@[simp] axiom s1458 (x : Prop) : f (g1459 x) = f (g1458 x)
@[simp] axiom s1459 (x : Prop) : f (g1460 x) = f (g1459 x)
@[simp] axiom s1460 (x : Prop) : f (g1461 x) = f (g1460 x)
@[simp] axiom s1461 (x : Prop) : f (g1462 x) = f (g1461 x)
@[simp] axiom s1462 (x : Prop) : f (g1463 x) = f (g1462 x)
@[simp] axiom s1463 (x : Prop) : f (g1464 x) = f (g1463 x)
@[simp] axiom s1464 (x : Prop) : f (g1465 x) = f (g1464 x)
@[simp] axiom s1465 (x : Prop) : f (g1466 x) = f (g1465 x)
@[simp] axiom s1466 (x : Prop) : f (g1467 x) = f (g1466 x)
@[simp] axiom s1467 (x : Prop) : f (g1468 x) = f (g1467 x)
@[simp] axiom s1468 (x : Prop) : f (g1469 x) = f (g1468 x)
@[simp] axiom s1469 (x : Prop) : f (g1470 x) = f (g1469 x)
@[simp] axiom s1470 (x : Prop) : f (g1471 x) = f (g1470 x)
@[simp] axiom s1471 (x : Prop) : f (g1472 x) = f (g1471 x)
@[simp] axiom s1472 (x : Prop) : f (g1473 x) = f (g1472 x)
@[simp] axiom s1473 (x : Prop) : f (g1474 x) = f (g1473 x)
@[simp] axiom s1474 (x : Prop) : f (g1475 x) = f (g1474 x)
@[simp] axiom s1475 (x : Prop) : f (g1476 x) = f (g1475 x)
@[simp] axiom s1476 (x : Prop) : f (g1477 x) = f (g1476 x)
@[simp] axiom s1477 (x : Prop) : f (g1478 x) = f (g1477 x)
@[simp] axiom s1478 (x : Prop) : f (g1479 x) = f (g1478 x)
@[simp] axiom s1479 (x : Prop) : f (g1480 x) = f (g1479 x)
@[simp] axiom s1480 (x : Prop) : f (g1481 x) = f (g1480 x)
@[simp] axiom s1481 (x : Prop) : f (g1482 x) = f (g1481 x)
@[simp] axiom s1482 (x : Prop) : f (g1483 x) = f (g1482 x)
@[simp] axiom s1483 (x : Prop) : f (g1484 x) = f (g1483 x)
@[simp] axiom s1484 (x : Prop) : f (g1485 x) = f (g1484 x)
@[simp] axiom s1485 (x : Prop) : f (g1486 x) = f (g1485 x)
@[simp] axiom s1486 (x : Prop) : f (g1487 x) = f (g1486 x)
@[simp] axiom s1487 (x : Prop) : f (g1488 x) = f (g1487 x)
@[simp] axiom s1488 (x : Prop) : f (g1489 x) = f (g1488 x)
@[simp] axiom s1489 (x : Prop) : f (g1490 x) = f (g1489 x)
@[simp] axiom s1490 (x : Prop) : f (g1491 x) = f (g1490 x)
@[simp] axiom s1491 (x : Prop) : f (g1492 x) = f (g1491 x)
@[simp] axiom s1492 (x : Prop) : f (g1493 x) = f (g1492 x)
@[simp] axiom s1493 (x : Prop) : f (g1494 x) = f (g1493 x)
@[simp] axiom s1494 (x : Prop) : f (g1495 x) = f (g1494 x)
@[simp] axiom s1495 (x : Prop) : f (g1496 x) = f (g1495 x)
@[simp] axiom s1496 (x : Prop) : f (g1497 x) = f (g1496 x)
@[simp] axiom s1497 (x : Prop) : f (g1498 x) = f (g1497 x)
@[simp] axiom s1498 (x : Prop) : f (g1499 x) = f (g1498 x)
@[simp] axiom s1499 (x : Prop) : f (g1500 x) = f (g1499 x)
@[simp] axiom s1500 (x : Prop) : f (g1501 x) = f (g1500 x)
@[simp] axiom s1501 (x : Prop) : f (g1502 x) = f (g1501 x)
@[simp] axiom s1502 (x : Prop) : f (g1503 x) = f (g1502 x)
@[simp] axiom s1503 (x : Prop) : f (g1504 x) = f (g1503 x)
@[simp] axiom s1504 (x : Prop) : f (g1505 x) = f (g1504 x)
@[simp] axiom s1505 (x : Prop) : f (g1506 x) = f (g1505 x)
@[simp] axiom s1506 (x : Prop) : f (g1507 x) = f (g1506 x)
@[simp] axiom s1507 (x : Prop) : f (g1508 x) = f (g1507 x)
@[simp] axiom s1508 (x : Prop) : f (g1509 x) = f (g1508 x)
@[simp] axiom s1509 (x : Prop) : f (g1510 x) = f (g1509 x)
@[simp] axiom s1510 (x : Prop) : f (g1511 x) = f (g1510 x)
@[simp] axiom s1511 (x : Prop) : f (g1512 x) = f (g1511 x)
@[simp] axiom s1512 (x : Prop) : f (g1513 x) = f (g1512 x)
@[simp] axiom s1513 (x : Prop) : f (g1514 x) = f (g1513 x)
@[simp] axiom s1514 (x : Prop) : f (g1515 x) = f (g1514 x)
@[simp] axiom s1515 (x : Prop) : f (g1516 x) = f (g1515 x)
@[simp] axiom s1516 (x : Prop) : f (g1517 x) = f (g1516 x)
@[simp] axiom s1517 (x : Prop) : f (g1518 x) = f (g1517 x)
@[simp] axiom s1518 (x : Prop) : f (g1519 x) = f (g1518 x)
@[simp] axiom s1519 (x : Prop) : f (g1520 x) = f (g1519 x)
@[simp] axiom s1520 (x : Prop) : f (g1521 x) = f (g1520 x)
@[simp] axiom s1521 (x : Prop) : f (g1522 x) = f (g1521 x)
@[simp] axiom s1522 (x : Prop) : f (g1523 x) = f (g1522 x)
@[simp] axiom s1523 (x : Prop) : f (g1524 x) = f (g1523 x)
@[simp] axiom s1524 (x : Prop) : f (g1525 x) = f (g1524 x)
@[simp] axiom s1525 (x : Prop) : f (g1526 x) = f (g1525 x)
@[simp] axiom s1526 (x : Prop) : f (g1527 x) = f (g1526 x)
@[simp] axiom s1527 (x : Prop) : f (g1528 x) = f (g1527 x)
@[simp] axiom s1528 (x : Prop) : f (g1529 x) = f (g1528 x)
@[simp] axiom s1529 (x : Prop) : f (g1530 x) = f (g1529 x)
@[simp] axiom s1530 (x : Prop) : f (g1531 x) = f (g1530 x)
@[simp] axiom s1531 (x : Prop) : f (g1532 x) = f (g1531 x)
@[simp] axiom s1532 (x : Prop) : f (g1533 x) = f (g1532 x)
@[simp] axiom s1533 (x : Prop) : f (g1534 x) = f (g1533 x)
@[simp] axiom s1534 (x : Prop) : f (g1535 x) = f (g1534 x)
@[simp] axiom s1535 (x : Prop) : f (g1536 x) = f (g1535 x)
@[simp] axiom s1536 (x : Prop) : f (g1537 x) = f (g1536 x)
@[simp] axiom s1537 (x : Prop) : f (g1538 x) = f (g1537 x)
@[simp] axiom s1538 (x : Prop) : f (g1539 x) = f (g1538 x)
@[simp] axiom s1539 (x : Prop) : f (g1540 x) = f (g1539 x)
@[simp] axiom s1540 (x : Prop) : f (g1541 x) = f (g1540 x)
@[simp] axiom s1541 (x : Prop) : f (g1542 x) = f (g1541 x)
@[simp] axiom s1542 (x : Prop) : f (g1543 x) = f (g1542 x)
@[simp] axiom s1543 (x : Prop) : f (g1544 x) = f (g1543 x)
@[simp] axiom s1544 (x : Prop) : f (g1545 x) = f (g1544 x)
@[simp] axiom s1545 (x : Prop) : f (g1546 x) = f (g1545 x)
@[simp] axiom s1546 (x : Prop) : f (g1547 x) = f (g1546 x)
@[simp] axiom s1547 (x : Prop) : f (g1548 x) = f (g1547 x)
@[simp] axiom s1548 (x : Prop) : f (g1549 x) = f (g1548 x)
@[simp] axiom s1549 (x : Prop) : f (g1550 x) = f (g1549 x)
@[simp] axiom s1550 (x : Prop) : f (g1551 x) = f (g1550 x)
@[simp] axiom s1551 (x : Prop) : f (g1552 x) = f (g1551 x)
@[simp] axiom s1552 (x : Prop) : f (g1553 x) = f (g1552 x)
@[simp] axiom s1553 (x : Prop) : f (g1554 x) = f (g1553 x)
@[simp] axiom s1554 (x : Prop) : f (g1555 x) = f (g1554 x)
@[simp] axiom s1555 (x : Prop) : f (g1556 x) = f (g1555 x)
@[simp] axiom s1556 (x : Prop) : f (g1557 x) = f (g1556 x)
@[simp] axiom s1557 (x : Prop) : f (g1558 x) = f (g1557 x)
@[simp] axiom s1558 (x : Prop) : f (g1559 x) = f (g1558 x)
@[simp] axiom s1559 (x : Prop) : f (g1560 x) = f (g1559 x)
@[simp] axiom s1560 (x : Prop) : f (g1561 x) = f (g1560 x)
@[simp] axiom s1561 (x : Prop) : f (g1562 x) = f (g1561 x)
@[simp] axiom s1562 (x : Prop) : f (g1563 x) = f (g1562 x)
@[simp] axiom s1563 (x : Prop) : f (g1564 x) = f (g1563 x)
@[simp] axiom s1564 (x : Prop) : f (g1565 x) = f (g1564 x)
@[simp] axiom s1565 (x : Prop) : f (g1566 x) = f (g1565 x)
@[simp] axiom s1566 (x : Prop) : f (g1567 x) = f (g1566 x)
@[simp] axiom s1567 (x : Prop) : f (g1568 x) = f (g1567 x)
@[simp] axiom s1568 (x : Prop) : f (g1569 x) = f (g1568 x)
@[simp] axiom s1569 (x : Prop) : f (g1570 x) = f (g1569 x)
@[simp] axiom s1570 (x : Prop) : f (g1571 x) = f (g1570 x)
@[simp] axiom s1571 (x : Prop) : f (g1572 x) = f (g1571 x)
@[simp] axiom s1572 (x : Prop) : f (g1573 x) = f (g1572 x)
@[simp] axiom s1573 (x : Prop) : f (g1574 x) = f (g1573 x)
@[simp] axiom s1574 (x : Prop) : f (g1575 x) = f (g1574 x)
@[simp] axiom s1575 (x : Prop) : f (g1576 x) = f (g1575 x)
@[simp] axiom s1576 (x : Prop) : f (g1577 x) = f (g1576 x)
@[simp] axiom s1577 (x : Prop) : f (g1578 x) = f (g1577 x)
@[simp] axiom s1578 (x : Prop) : f (g1579 x) = f (g1578 x)
@[simp] axiom s1579 (x : Prop) : f (g1580 x) = f (g1579 x)
@[simp] axiom s1580 (x : Prop) : f (g1581 x) = f (g1580 x)
@[simp] axiom s1581 (x : Prop) : f (g1582 x) = f (g1581 x)
@[simp] axiom s1582 (x : Prop) : f (g1583 x) = f (g1582 x)
@[simp] axiom s1583 (x : Prop) : f (g1584 x) = f (g1583 x)
@[simp] axiom s1584 (x : Prop) : f (g1585 x) = f (g1584 x)
@[simp] axiom s1585 (x : Prop) : f (g1586 x) = f (g1585 x)
@[simp] axiom s1586 (x : Prop) : f (g1587 x) = f (g1586 x)
@[simp] axiom s1587 (x : Prop) : f (g1588 x) = f (g1587 x)
@[simp] axiom s1588 (x : Prop) : f (g1589 x) = f (g1588 x)
@[simp] axiom s1589 (x : Prop) : f (g1590 x) = f (g1589 x)
@[simp] axiom s1590 (x : Prop) : f (g1591 x) = f (g1590 x)
@[simp] axiom s1591 (x : Prop) : f (g1592 x) = f (g1591 x)
@[simp] axiom s1592 (x : Prop) : f (g1593 x) = f (g1592 x)
@[simp] axiom s1593 (x : Prop) : f (g1594 x) = f (g1593 x)
@[simp] axiom s1594 (x : Prop) : f (g1595 x) = f (g1594 x)
@[simp] axiom s1595 (x : Prop) : f (g1596 x) = f (g1595 x)
@[simp] axiom s1596 (x : Prop) : f (g1597 x) = f (g1596 x)
@[simp] axiom s1597 (x : Prop) : f (g1598 x) = f (g1597 x)
@[simp] axiom s1598 (x : Prop) : f (g1599 x) = f (g1598 x)
@[simp] axiom s1599 (x : Prop) : f (g1600 x) = f (g1599 x)
@[simp] axiom s1600 (x : Prop) : f (g1601 x) = f (g1600 x)
@[simp] axiom s1601 (x : Prop) : f (g1602 x) = f (g1601 x)
@[simp] axiom s1602 (x : Prop) : f (g1603 x) = f (g1602 x)
@[simp] axiom s1603 (x : Prop) : f (g1604 x) = f (g1603 x)
@[simp] axiom s1604 (x : Prop) : f (g1605 x) = f (g1604 x)
@[simp] axiom s1605 (x : Prop) : f (g1606 x) = f (g1605 x)
@[simp] axiom s1606 (x : Prop) : f (g1607 x) = f (g1606 x)
@[simp] axiom s1607 (x : Prop) : f (g1608 x) = f (g1607 x)
@[simp] axiom s1608 (x : Prop) : f (g1609 x) = f (g1608 x)
@[simp] axiom s1609 (x : Prop) : f (g1610 x) = f (g1609 x)
@[simp] axiom s1610 (x : Prop) : f (g1611 x) = f (g1610 x)
@[simp] axiom s1611 (x : Prop) : f (g1612 x) = f (g1611 x)
@[simp] axiom s1612 (x : Prop) : f (g1613 x) = f (g1612 x)
@[simp] axiom s1613 (x : Prop) : f (g1614 x) = f (g1613 x)
@[simp] axiom s1614 (x : Prop) : f (g1615 x) = f (g1614 x)
@[simp] axiom s1615 (x : Prop) : f (g1616 x) = f (g1615 x)
@[simp] axiom s1616 (x : Prop) : f (g1617 x) = f (g1616 x)
@[simp] axiom s1617 (x : Prop) : f (g1618 x) = f (g1617 x)
@[simp] axiom s1618 (x : Prop) : f (g1619 x) = f (g1618 x)
@[simp] axiom s1619 (x : Prop) : f (g1620 x) = f (g1619 x)
@[simp] axiom s1620 (x : Prop) : f (g1621 x) = f (g1620 x)
@[simp] axiom s1621 (x : Prop) : f (g1622 x) = f (g1621 x)
@[simp] axiom s1622 (x : Prop) : f (g1623 x) = f (g1622 x)
@[simp] axiom s1623 (x : Prop) : f (g1624 x) = f (g1623 x)
@[simp] axiom s1624 (x : Prop) : f (g1625 x) = f (g1624 x)
@[simp] axiom s1625 (x : Prop) : f (g1626 x) = f (g1625 x)
@[simp] axiom s1626 (x : Prop) : f (g1627 x) = f (g1626 x)
@[simp] axiom s1627 (x : Prop) : f (g1628 x) = f (g1627 x)
@[simp] axiom s1628 (x : Prop) : f (g1629 x) = f (g1628 x)
@[simp] axiom s1629 (x : Prop) : f (g1630 x) = f (g1629 x)
@[simp] axiom s1630 (x : Prop) : f (g1631 x) = f (g1630 x)
@[simp] axiom s1631 (x : Prop) : f (g1632 x) = f (g1631 x)
@[simp] axiom s1632 (x : Prop) : f (g1633 x) = f (g1632 x)
@[simp] axiom s1633 (x : Prop) : f (g1634 x) = f (g1633 x)
@[simp] axiom s1634 (x : Prop) : f (g1635 x) = f (g1634 x)
@[simp] axiom s1635 (x : Prop) : f (g1636 x) = f (g1635 x)
@[simp] axiom s1636 (x : Prop) : f (g1637 x) = f (g1636 x)
@[simp] axiom s1637 (x : Prop) : f (g1638 x) = f (g1637 x)
@[simp] axiom s1638 (x : Prop) : f (g1639 x) = f (g1638 x)
@[simp] axiom s1639 (x : Prop) : f (g1640 x) = f (g1639 x)
@[simp] axiom s1640 (x : Prop) : f (g1641 x) = f (g1640 x)
@[simp] axiom s1641 (x : Prop) : f (g1642 x) = f (g1641 x)
@[simp] axiom s1642 (x : Prop) : f (g1643 x) = f (g1642 x)
@[simp] axiom s1643 (x : Prop) : f (g1644 x) = f (g1643 x)
@[simp] axiom s1644 (x : Prop) : f (g1645 x) = f (g1644 x)
@[simp] axiom s1645 (x : Prop) : f (g1646 x) = f (g1645 x)
@[simp] axiom s1646 (x : Prop) : f (g1647 x) = f (g1646 x)
@[simp] axiom s1647 (x : Prop) : f (g1648 x) = f (g1647 x)
@[simp] axiom s1648 (x : Prop) : f (g1649 x) = f (g1648 x)
@[simp] axiom s1649 (x : Prop) : f (g1650 x) = f (g1649 x)
@[simp] axiom s1650 (x : Prop) : f (g1651 x) = f (g1650 x)
@[simp] axiom s1651 (x : Prop) : f (g1652 x) = f (g1651 x)
@[simp] axiom s1652 (x : Prop) : f (g1653 x) = f (g1652 x)
@[simp] axiom s1653 (x : Prop) : f (g1654 x) = f (g1653 x)
@[simp] axiom s1654 (x : Prop) : f (g1655 x) = f (g1654 x)
@[simp] axiom s1655 (x : Prop) : f (g1656 x) = f (g1655 x)
@[simp] axiom s1656 (x : Prop) : f (g1657 x) = f (g1656 x)
@[simp] axiom s1657 (x : Prop) : f (g1658 x) = f (g1657 x)
@[simp] axiom s1658 (x : Prop) : f (g1659 x) = f (g1658 x)
@[simp] axiom s1659 (x : Prop) : f (g1660 x) = f (g1659 x)
@[simp] axiom s1660 (x : Prop) : f (g1661 x) = f (g1660 x)
@[simp] axiom s1661 (x : Prop) : f (g1662 x) = f (g1661 x)
@[simp] axiom s1662 (x : Prop) : f (g1663 x) = f (g1662 x)
@[simp] axiom s1663 (x : Prop) : f (g1664 x) = f (g1663 x)
@[simp] axiom s1664 (x : Prop) : f (g1665 x) = f (g1664 x)
@[simp] axiom s1665 (x : Prop) : f (g1666 x) = f (g1665 x)
@[simp] axiom s1666 (x : Prop) : f (g1667 x) = f (g1666 x)
@[simp] axiom s1667 (x : Prop) : f (g1668 x) = f (g1667 x)
@[simp] axiom s1668 (x : Prop) : f (g1669 x) = f (g1668 x)
@[simp] axiom s1669 (x : Prop) : f (g1670 x) = f (g1669 x)
@[simp] axiom s1670 (x : Prop) : f (g1671 x) = f (g1670 x)
@[simp] axiom s1671 (x : Prop) : f (g1672 x) = f (g1671 x)
@[simp] axiom s1672 (x : Prop) : f (g1673 x) = f (g1672 x)
@[simp] axiom s1673 (x : Prop) : f (g1674 x) = f (g1673 x)
@[simp] axiom s1674 (x : Prop) : f (g1675 x) = f (g1674 x)
@[simp] axiom s1675 (x : Prop) : f (g1676 x) = f (g1675 x)
@[simp] axiom s1676 (x : Prop) : f (g1677 x) = f (g1676 x)
@[simp] axiom s1677 (x : Prop) : f (g1678 x) = f (g1677 x)
@[simp] axiom s1678 (x : Prop) : f (g1679 x) = f (g1678 x)
@[simp] axiom s1679 (x : Prop) : f (g1680 x) = f (g1679 x)
@[simp] axiom s1680 (x : Prop) : f (g1681 x) = f (g1680 x)
@[simp] axiom s1681 (x : Prop) : f (g1682 x) = f (g1681 x)
@[simp] axiom s1682 (x : Prop) : f (g1683 x) = f (g1682 x)
@[simp] axiom s1683 (x : Prop) : f (g1684 x) = f (g1683 x)
@[simp] axiom s1684 (x : Prop) : f (g1685 x) = f (g1684 x)
@[simp] axiom s1685 (x : Prop) : f (g1686 x) = f (g1685 x)
@[simp] axiom s1686 (x : Prop) : f (g1687 x) = f (g1686 x)
@[simp] axiom s1687 (x : Prop) : f (g1688 x) = f (g1687 x)
@[simp] axiom s1688 (x : Prop) : f (g1689 x) = f (g1688 x)
@[simp] axiom s1689 (x : Prop) : f (g1690 x) = f (g1689 x)
@[simp] axiom s1690 (x : Prop) : f (g1691 x) = f (g1690 x)
@[simp] axiom s1691 (x : Prop) : f (g1692 x) = f (g1691 x)
@[simp] axiom s1692 (x : Prop) : f (g1693 x) = f (g1692 x)
@[simp] axiom s1693 (x : Prop) : f (g1694 x) = f (g1693 x)
@[simp] axiom s1694 (x : Prop) : f (g1695 x) = f (g1694 x)
@[simp] axiom s1695 (x : Prop) : f (g1696 x) = f (g1695 x)
@[simp] axiom s1696 (x : Prop) : f (g1697 x) = f (g1696 x)
@[simp] axiom s1697 (x : Prop) : f (g1698 x) = f (g1697 x)
@[simp] axiom s1698 (x : Prop) : f (g1699 x) = f (g1698 x)
@[simp] axiom s1699 (x : Prop) : f (g1700 x) = f (g1699 x)
@[simp] axiom s1700 (x : Prop) : f (g1701 x) = f (g1700 x)
@[simp] axiom s1701 (x : Prop) : f (g1702 x) = f (g1701 x)
@[simp] axiom s1702 (x : Prop) : f (g1703 x) = f (g1702 x)
@[simp] axiom s1703 (x : Prop) : f (g1704 x) = f (g1703 x)
@[simp] axiom s1704 (x : Prop) : f (g1705 x) = f (g1704 x)
@[simp] axiom s1705 (x : Prop) : f (g1706 x) = f (g1705 x)
@[simp] axiom s1706 (x : Prop) : f (g1707 x) = f (g1706 x)
@[simp] axiom s1707 (x : Prop) : f (g1708 x) = f (g1707 x)
@[simp] axiom s1708 (x : Prop) : f (g1709 x) = f (g1708 x)
@[simp] axiom s1709 (x : Prop) : f (g1710 x) = f (g1709 x)
@[simp] axiom s1710 (x : Prop) : f (g1711 x) = f (g1710 x)
@[simp] axiom s1711 (x : Prop) : f (g1712 x) = f (g1711 x)
@[simp] axiom s1712 (x : Prop) : f (g1713 x) = f (g1712 x)
@[simp] axiom s1713 (x : Prop) : f (g1714 x) = f (g1713 x)
@[simp] axiom s1714 (x : Prop) : f (g1715 x) = f (g1714 x)
@[simp] axiom s1715 (x : Prop) : f (g1716 x) = f (g1715 x)
@[simp] axiom s1716 (x : Prop) : f (g1717 x) = f (g1716 x)
@[simp] axiom s1717 (x : Prop) : f (g1718 x) = f (g1717 x)
@[simp] axiom s1718 (x : Prop) : f (g1719 x) = f (g1718 x)
@[simp] axiom s1719 (x : Prop) : f (g1720 x) = f (g1719 x)
@[simp] axiom s1720 (x : Prop) : f (g1721 x) = f (g1720 x)
@[simp] axiom s1721 (x : Prop) : f (g1722 x) = f (g1721 x)
@[simp] axiom s1722 (x : Prop) : f (g1723 x) = f (g1722 x)
@[simp] axiom s1723 (x : Prop) : f (g1724 x) = f (g1723 x)
@[simp] axiom s1724 (x : Prop) : f (g1725 x) = f (g1724 x)
@[simp] axiom s1725 (x : Prop) : f (g1726 x) = f (g1725 x)
@[simp] axiom s1726 (x : Prop) : f (g1727 x) = f (g1726 x)
@[simp] axiom s1727 (x : Prop) : f (g1728 x) = f (g1727 x)
@[simp] axiom s1728 (x : Prop) : f (g1729 x) = f (g1728 x)
@[simp] axiom s1729 (x : Prop) : f (g1730 x) = f (g1729 x)
@[simp] axiom s1730 (x : Prop) : f (g1731 x) = f (g1730 x)
@[simp] axiom s1731 (x : Prop) : f (g1732 x) = f (g1731 x)
@[simp] axiom s1732 (x : Prop) : f (g1733 x) = f (g1732 x)
@[simp] axiom s1733 (x : Prop) : f (g1734 x) = f (g1733 x)
@[simp] axiom s1734 (x : Prop) : f (g1735 x) = f (g1734 x)
@[simp] axiom s1735 (x : Prop) : f (g1736 x) = f (g1735 x)
@[simp] axiom s1736 (x : Prop) : f (g1737 x) = f (g1736 x)
@[simp] axiom s1737 (x : Prop) : f (g1738 x) = f (g1737 x)
@[simp] axiom s1738 (x : Prop) : f (g1739 x) = f (g1738 x)
@[simp] axiom s1739 (x : Prop) : f (g1740 x) = f (g1739 x)
@[simp] axiom s1740 (x : Prop) : f (g1741 x) = f (g1740 x)
@[simp] axiom s1741 (x : Prop) : f (g1742 x) = f (g1741 x)
@[simp] axiom s1742 (x : Prop) : f (g1743 x) = f (g1742 x)
@[simp] axiom s1743 (x : Prop) : f (g1744 x) = f (g1743 x)
@[simp] axiom s1744 (x : Prop) : f (g1745 x) = f (g1744 x)
@[simp] axiom s1745 (x : Prop) : f (g1746 x) = f (g1745 x)
@[simp] axiom s1746 (x : Prop) : f (g1747 x) = f (g1746 x)
@[simp] axiom s1747 (x : Prop) : f (g1748 x) = f (g1747 x)
@[simp] axiom s1748 (x : Prop) : f (g1749 x) = f (g1748 x)
@[simp] axiom s1749 (x : Prop) : f (g1750 x) = f (g1749 x)
@[simp] axiom s1750 (x : Prop) : f (g1751 x) = f (g1750 x)
@[simp] axiom s1751 (x : Prop) : f (g1752 x) = f (g1751 x)
@[simp] axiom s1752 (x : Prop) : f (g1753 x) = f (g1752 x)
@[simp] axiom s1753 (x : Prop) : f (g1754 x) = f (g1753 x)
@[simp] axiom s1754 (x : Prop) : f (g1755 x) = f (g1754 x)
@[simp] axiom s1755 (x : Prop) : f (g1756 x) = f (g1755 x)
@[simp] axiom s1756 (x : Prop) : f (g1757 x) = f (g1756 x)
@[simp] axiom s1757 (x : Prop) : f (g1758 x) = f (g1757 x)
@[simp] axiom s1758 (x : Prop) : f (g1759 x) = f (g1758 x)
@[simp] axiom s1759 (x : Prop) : f (g1760 x) = f (g1759 x)
@[simp] axiom s1760 (x : Prop) : f (g1761 x) = f (g1760 x)
@[simp] axiom s1761 (x : Prop) : f (g1762 x) = f (g1761 x)
@[simp] axiom s1762 (x : Prop) : f (g1763 x) = f (g1762 x)
@[simp] axiom s1763 (x : Prop) : f (g1764 x) = f (g1763 x)
@[simp] axiom s1764 (x : Prop) : f (g1765 x) = f (g1764 x)
@[simp] axiom s1765 (x : Prop) : f (g1766 x) = f (g1765 x)
@[simp] axiom s1766 (x : Prop) : f (g1767 x) = f (g1766 x)
@[simp] axiom s1767 (x : Prop) : f (g1768 x) = f (g1767 x)
@[simp] axiom s1768 (x : Prop) : f (g1769 x) = f (g1768 x)
@[simp] axiom s1769 (x : Prop) : f (g1770 x) = f (g1769 x)
@[simp] axiom s1770 (x : Prop) : f (g1771 x) = f (g1770 x)
@[simp] axiom s1771 (x : Prop) : f (g1772 x) = f (g1771 x)
@[simp] axiom s1772 (x : Prop) : f (g1773 x) = f (g1772 x)
@[simp] axiom s1773 (x : Prop) : f (g1774 x) = f (g1773 x)
@[simp] axiom s1774 (x : Prop) : f (g1775 x) = f (g1774 x)
@[simp] axiom s1775 (x : Prop) : f (g1776 x) = f (g1775 x)
@[simp] axiom s1776 (x : Prop) : f (g1777 x) = f (g1776 x)
@[simp] axiom s1777 (x : Prop) : f (g1778 x) = f (g1777 x)
@[simp] axiom s1778 (x : Prop) : f (g1779 x) = f (g1778 x)
@[simp] axiom s1779 (x : Prop) : f (g1780 x) = f (g1779 x)
@[simp] axiom s1780 (x : Prop) : f (g1781 x) = f (g1780 x)
@[simp] axiom s1781 (x : Prop) : f (g1782 x) = f (g1781 x)
@[simp] axiom s1782 (x : Prop) : f (g1783 x) = f (g1782 x)
@[simp] axiom s1783 (x : Prop) : f (g1784 x) = f (g1783 x)
@[simp] axiom s1784 (x : Prop) : f (g1785 x) = f (g1784 x)
@[simp] axiom s1785 (x : Prop) : f (g1786 x) = f (g1785 x)
@[simp] axiom s1786 (x : Prop) : f (g1787 x) = f (g1786 x)
@[simp] axiom s1787 (x : Prop) : f (g1788 x) = f (g1787 x)
@[simp] axiom s1788 (x : Prop) : f (g1789 x) = f (g1788 x)
@[simp] axiom s1789 (x : Prop) : f (g1790 x) = f (g1789 x)
@[simp] axiom s1790 (x : Prop) : f (g1791 x) = f (g1790 x)
@[simp] axiom s1791 (x : Prop) : f (g1792 x) = f (g1791 x)
@[simp] axiom s1792 (x : Prop) : f (g1793 x) = f (g1792 x)
@[simp] axiom s1793 (x : Prop) : f (g1794 x) = f (g1793 x)
@[simp] axiom s1794 (x : Prop) : f (g1795 x) = f (g1794 x)
@[simp] axiom s1795 (x : Prop) : f (g1796 x) = f (g1795 x)
@[simp] axiom s1796 (x : Prop) : f (g1797 x) = f (g1796 x)
@[simp] axiom s1797 (x : Prop) : f (g1798 x) = f (g1797 x)
@[simp] axiom s1798 (x : Prop) : f (g1799 x) = f (g1798 x)
@[simp] axiom s1799 (x : Prop) : f (g1800 x) = f (g1799 x)
@[simp] axiom s1800 (x : Prop) : f (g1801 x) = f (g1800 x)
@[simp] axiom s1801 (x : Prop) : f (g1802 x) = f (g1801 x)
@[simp] axiom s1802 (x : Prop) : f (g1803 x) = f (g1802 x)
@[simp] axiom s1803 (x : Prop) : f (g1804 x) = f (g1803 x)
@[simp] axiom s1804 (x : Prop) : f (g1805 x) = f (g1804 x)
@[simp] axiom s1805 (x : Prop) : f (g1806 x) = f (g1805 x)
@[simp] axiom s1806 (x : Prop) : f (g1807 x) = f (g1806 x)
@[simp] axiom s1807 (x : Prop) : f (g1808 x) = f (g1807 x)
@[simp] axiom s1808 (x : Prop) : f (g1809 x) = f (g1808 x)
@[simp] axiom s1809 (x : Prop) : f (g1810 x) = f (g1809 x)
@[simp] axiom s1810 (x : Prop) : f (g1811 x) = f (g1810 x)
@[simp] axiom s1811 (x : Prop) : f (g1812 x) = f (g1811 x)
@[simp] axiom s1812 (x : Prop) : f (g1813 x) = f (g1812 x)
@[simp] axiom s1813 (x : Prop) : f (g1814 x) = f (g1813 x)
@[simp] axiom s1814 (x : Prop) : f (g1815 x) = f (g1814 x)
@[simp] axiom s1815 (x : Prop) : f (g1816 x) = f (g1815 x)
@[simp] axiom s1816 (x : Prop) : f (g1817 x) = f (g1816 x)
@[simp] axiom s1817 (x : Prop) : f (g1818 x) = f (g1817 x)
@[simp] axiom s1818 (x : Prop) : f (g1819 x) = f (g1818 x)
@[simp] axiom s1819 (x : Prop) : f (g1820 x) = f (g1819 x)
@[simp] axiom s1820 (x : Prop) : f (g1821 x) = f (g1820 x)
@[simp] axiom s1821 (x : Prop) : f (g1822 x) = f (g1821 x)
@[simp] axiom s1822 (x : Prop) : f (g1823 x) = f (g1822 x)
@[simp] axiom s1823 (x : Prop) : f (g1824 x) = f (g1823 x)
@[simp] axiom s1824 (x : Prop) : f (g1825 x) = f (g1824 x)
@[simp] axiom s1825 (x : Prop) : f (g1826 x) = f (g1825 x)
@[simp] axiom s1826 (x : Prop) : f (g1827 x) = f (g1826 x)
@[simp] axiom s1827 (x : Prop) : f (g1828 x) = f (g1827 x)
@[simp] axiom s1828 (x : Prop) : f (g1829 x) = f (g1828 x)
@[simp] axiom s1829 (x : Prop) : f (g1830 x) = f (g1829 x)
@[simp] axiom s1830 (x : Prop) : f (g1831 x) = f (g1830 x)
@[simp] axiom s1831 (x : Prop) : f (g1832 x) = f (g1831 x)
@[simp] axiom s1832 (x : Prop) : f (g1833 x) = f (g1832 x)
@[simp] axiom s1833 (x : Prop) : f (g1834 x) = f (g1833 x)
@[simp] axiom s1834 (x : Prop) : f (g1835 x) = f (g1834 x)
@[simp] axiom s1835 (x : Prop) : f (g1836 x) = f (g1835 x)
@[simp] axiom s1836 (x : Prop) : f (g1837 x) = f (g1836 x)
@[simp] axiom s1837 (x : Prop) : f (g1838 x) = f (g1837 x)
@[simp] axiom s1838 (x : Prop) : f (g1839 x) = f (g1838 x)
@[simp] axiom s1839 (x : Prop) : f (g1840 x) = f (g1839 x)
@[simp] axiom s1840 (x : Prop) : f (g1841 x) = f (g1840 x)
@[simp] axiom s1841 (x : Prop) : f (g1842 x) = f (g1841 x)
@[simp] axiom s1842 (x : Prop) : f (g1843 x) = f (g1842 x)
@[simp] axiom s1843 (x : Prop) : f (g1844 x) = f (g1843 x)
@[simp] axiom s1844 (x : Prop) : f (g1845 x) = f (g1844 x)
@[simp] axiom s1845 (x : Prop) : f (g1846 x) = f (g1845 x)
@[simp] axiom s1846 (x : Prop) : f (g1847 x) = f (g1846 x)
@[simp] axiom s1847 (x : Prop) : f (g1848 x) = f (g1847 x)
@[simp] axiom s1848 (x : Prop) : f (g1849 x) = f (g1848 x)
@[simp] axiom s1849 (x : Prop) : f (g1850 x) = f (g1849 x)
@[simp] axiom s1850 (x : Prop) : f (g1851 x) = f (g1850 x)
@[simp] axiom s1851 (x : Prop) : f (g1852 x) = f (g1851 x)
@[simp] axiom s1852 (x : Prop) : f (g1853 x) = f (g1852 x)
@[simp] axiom s1853 (x : Prop) : f (g1854 x) = f (g1853 x)
@[simp] axiom s1854 (x : Prop) : f (g1855 x) = f (g1854 x)
@[simp] axiom s1855 (x : Prop) : f (g1856 x) = f (g1855 x)
@[simp] axiom s1856 (x : Prop) : f (g1857 x) = f (g1856 x)
@[simp] axiom s1857 (x : Prop) : f (g1858 x) = f (g1857 x)
@[simp] axiom s1858 (x : Prop) : f (g1859 x) = f (g1858 x)
@[simp] axiom s1859 (x : Prop) : f (g1860 x) = f (g1859 x)
@[simp] axiom s1860 (x : Prop) : f (g1861 x) = f (g1860 x)
@[simp] axiom s1861 (x : Prop) : f (g1862 x) = f (g1861 x)
@[simp] axiom s1862 (x : Prop) : f (g1863 x) = f (g1862 x)
@[simp] axiom s1863 (x : Prop) : f (g1864 x) = f (g1863 x)
@[simp] axiom s1864 (x : Prop) : f (g1865 x) = f (g1864 x)
@[simp] axiom s1865 (x : Prop) : f (g1866 x) = f (g1865 x)
@[simp] axiom s1866 (x : Prop) : f (g1867 x) = f (g1866 x)
@[simp] axiom s1867 (x : Prop) : f (g1868 x) = f (g1867 x)
@[simp] axiom s1868 (x : Prop) : f (g1869 x) = f (g1868 x)
@[simp] axiom s1869 (x : Prop) : f (g1870 x) = f (g1869 x)
@[simp] axiom s1870 (x : Prop) : f (g1871 x) = f (g1870 x)
@[simp] axiom s1871 (x : Prop) : f (g1872 x) = f (g1871 x)
@[simp] axiom s1872 (x : Prop) : f (g1873 x) = f (g1872 x)
@[simp] axiom s1873 (x : Prop) : f (g1874 x) = f (g1873 x)
@[simp] axiom s1874 (x : Prop) : f (g1875 x) = f (g1874 x)
@[simp] axiom s1875 (x : Prop) : f (g1876 x) = f (g1875 x)
@[simp] axiom s1876 (x : Prop) : f (g1877 x) = f (g1876 x)
@[simp] axiom s1877 (x : Prop) : f (g1878 x) = f (g1877 x)
@[simp] axiom s1878 (x : Prop) : f (g1879 x) = f (g1878 x)
@[simp] axiom s1879 (x : Prop) : f (g1880 x) = f (g1879 x)
@[simp] axiom s1880 (x : Prop) : f (g1881 x) = f (g1880 x)
@[simp] axiom s1881 (x : Prop) : f (g1882 x) = f (g1881 x)
@[simp] axiom s1882 (x : Prop) : f (g1883 x) = f (g1882 x)
@[simp] axiom s1883 (x : Prop) : f (g1884 x) = f (g1883 x)
@[simp] axiom s1884 (x : Prop) : f (g1885 x) = f (g1884 x)
@[simp] axiom s1885 (x : Prop) : f (g1886 x) = f (g1885 x)
@[simp] axiom s1886 (x : Prop) : f (g1887 x) = f (g1886 x)
@[simp] axiom s1887 (x : Prop) : f (g1888 x) = f (g1887 x)
@[simp] axiom s1888 (x : Prop) : f (g1889 x) = f (g1888 x)
@[simp] axiom s1889 (x : Prop) : f (g1890 x) = f (g1889 x)
@[simp] axiom s1890 (x : Prop) : f (g1891 x) = f (g1890 x)
@[simp] axiom s1891 (x : Prop) : f (g1892 x) = f (g1891 x)
@[simp] axiom s1892 (x : Prop) : f (g1893 x) = f (g1892 x)
@[simp] axiom s1893 (x : Prop) : f (g1894 x) = f (g1893 x)
@[simp] axiom s1894 (x : Prop) : f (g1895 x) = f (g1894 x)
@[simp] axiom s1895 (x : Prop) : f (g1896 x) = f (g1895 x)
@[simp] axiom s1896 (x : Prop) : f (g1897 x) = f (g1896 x)
@[simp] axiom s1897 (x : Prop) : f (g1898 x) = f (g1897 x)
@[simp] axiom s1898 (x : Prop) : f (g1899 x) = f (g1898 x)
@[simp] axiom s1899 (x : Prop) : f (g1900 x) = f (g1899 x)
@[simp] axiom s1900 (x : Prop) : f (g1901 x) = f (g1900 x)
@[simp] axiom s1901 (x : Prop) : f (g1902 x) = f (g1901 x)
@[simp] axiom s1902 (x : Prop) : f (g1903 x) = f (g1902 x)
@[simp] axiom s1903 (x : Prop) : f (g1904 x) = f (g1903 x)
@[simp] axiom s1904 (x : Prop) : f (g1905 x) = f (g1904 x)
@[simp] axiom s1905 (x : Prop) : f (g1906 x) = f (g1905 x)
@[simp] axiom s1906 (x : Prop) : f (g1907 x) = f (g1906 x)
@[simp] axiom s1907 (x : Prop) : f (g1908 x) = f (g1907 x)
@[simp] axiom s1908 (x : Prop) : f (g1909 x) = f (g1908 x)
@[simp] axiom s1909 (x : Prop) : f (g1910 x) = f (g1909 x)
@[simp] axiom s1910 (x : Prop) : f (g1911 x) = f (g1910 x)
@[simp] axiom s1911 (x : Prop) : f (g1912 x) = f (g1911 x)
@[simp] axiom s1912 (x : Prop) : f (g1913 x) = f (g1912 x)
@[simp] axiom s1913 (x : Prop) : f (g1914 x) = f (g1913 x)
@[simp] axiom s1914 (x : Prop) : f (g1915 x) = f (g1914 x)
@[simp] axiom s1915 (x : Prop) : f (g1916 x) = f (g1915 x)
@[simp] axiom s1916 (x : Prop) : f (g1917 x) = f (g1916 x)
@[simp] axiom s1917 (x : Prop) : f (g1918 x) = f (g1917 x)
@[simp] axiom s1918 (x : Prop) : f (g1919 x) = f (g1918 x)
@[simp] axiom s1919 (x : Prop) : f (g1920 x) = f (g1919 x)
@[simp] axiom s1920 (x : Prop) : f (g1921 x) = f (g1920 x)
@[simp] axiom s1921 (x : Prop) : f (g1922 x) = f (g1921 x)
@[simp] axiom s1922 (x : Prop) : f (g1923 x) = f (g1922 x)
@[simp] axiom s1923 (x : Prop) : f (g1924 x) = f (g1923 x)
@[simp] axiom s1924 (x : Prop) : f (g1925 x) = f (g1924 x)
@[simp] axiom s1925 (x : Prop) : f (g1926 x) = f (g1925 x)
@[simp] axiom s1926 (x : Prop) : f (g1927 x) = f (g1926 x)
@[simp] axiom s1927 (x : Prop) : f (g1928 x) = f (g1927 x)
@[simp] axiom s1928 (x : Prop) : f (g1929 x) = f (g1928 x)
@[simp] axiom s1929 (x : Prop) : f (g1930 x) = f (g1929 x)
@[simp] axiom s1930 (x : Prop) : f (g1931 x) = f (g1930 x)
@[simp] axiom s1931 (x : Prop) : f (g1932 x) = f (g1931 x)
@[simp] axiom s1932 (x : Prop) : f (g1933 x) = f (g1932 x)
@[simp] axiom s1933 (x : Prop) : f (g1934 x) = f (g1933 x)
@[simp] axiom s1934 (x : Prop) : f (g1935 x) = f (g1934 x)
@[simp] axiom s1935 (x : Prop) : f (g1936 x) = f (g1935 x)
@[simp] axiom s1936 (x : Prop) : f (g1937 x) = f (g1936 x)
@[simp] axiom s1937 (x : Prop) : f (g1938 x) = f (g1937 x)
@[simp] axiom s1938 (x : Prop) : f (g1939 x) = f (g1938 x)
@[simp] axiom s1939 (x : Prop) : f (g1940 x) = f (g1939 x)
@[simp] axiom s1940 (x : Prop) : f (g1941 x) = f (g1940 x)
@[simp] axiom s1941 (x : Prop) : f (g1942 x) = f (g1941 x)
@[simp] axiom s1942 (x : Prop) : f (g1943 x) = f (g1942 x)
@[simp] axiom s1943 (x : Prop) : f (g1944 x) = f (g1943 x)
@[simp] axiom s1944 (x : Prop) : f (g1945 x) = f (g1944 x)
@[simp] axiom s1945 (x : Prop) : f (g1946 x) = f (g1945 x)
@[simp] axiom s1946 (x : Prop) : f (g1947 x) = f (g1946 x)
@[simp] axiom s1947 (x : Prop) : f (g1948 x) = f (g1947 x)
@[simp] axiom s1948 (x : Prop) : f (g1949 x) = f (g1948 x)
@[simp] axiom s1949 (x : Prop) : f (g1950 x) = f (g1949 x)
@[simp] axiom s1950 (x : Prop) : f (g1951 x) = f (g1950 x)
@[simp] axiom s1951 (x : Prop) : f (g1952 x) = f (g1951 x)
@[simp] axiom s1952 (x : Prop) : f (g1953 x) = f (g1952 x)
@[simp] axiom s1953 (x : Prop) : f (g1954 x) = f (g1953 x)
@[simp] axiom s1954 (x : Prop) : f (g1955 x) = f (g1954 x)
@[simp] axiom s1955 (x : Prop) : f (g1956 x) = f (g1955 x)
@[simp] axiom s1956 (x : Prop) : f (g1957 x) = f (g1956 x)
@[simp] axiom s1957 (x : Prop) : f (g1958 x) = f (g1957 x)
@[simp] axiom s1958 (x : Prop) : f (g1959 x) = f (g1958 x)
@[simp] axiom s1959 (x : Prop) : f (g1960 x) = f (g1959 x)
@[simp] axiom s1960 (x : Prop) : f (g1961 x) = f (g1960 x)
@[simp] axiom s1961 (x : Prop) : f (g1962 x) = f (g1961 x)
@[simp] axiom s1962 (x : Prop) : f (g1963 x) = f (g1962 x)
@[simp] axiom s1963 (x : Prop) : f (g1964 x) = f (g1963 x)
@[simp] axiom s1964 (x : Prop) : f (g1965 x) = f (g1964 x)
@[simp] axiom s1965 (x : Prop) : f (g1966 x) = f (g1965 x)
@[simp] axiom s1966 (x : Prop) : f (g1967 x) = f (g1966 x)
@[simp] axiom s1967 (x : Prop) : f (g1968 x) = f (g1967 x)
@[simp] axiom s1968 (x : Prop) : f (g1969 x) = f (g1968 x)
@[simp] axiom s1969 (x : Prop) : f (g1970 x) = f (g1969 x)
@[simp] axiom s1970 (x : Prop) : f (g1971 x) = f (g1970 x)
@[simp] axiom s1971 (x : Prop) : f (g1972 x) = f (g1971 x)
@[simp] axiom s1972 (x : Prop) : f (g1973 x) = f (g1972 x)
@[simp] axiom s1973 (x : Prop) : f (g1974 x) = f (g1973 x)
@[simp] axiom s1974 (x : Prop) : f (g1975 x) = f (g1974 x)
@[simp] axiom s1975 (x : Prop) : f (g1976 x) = f (g1975 x)
@[simp] axiom s1976 (x : Prop) : f (g1977 x) = f (g1976 x)
@[simp] axiom s1977 (x : Prop) : f (g1978 x) = f (g1977 x)
@[simp] axiom s1978 (x : Prop) : f (g1979 x) = f (g1978 x)
@[simp] axiom s1979 (x : Prop) : f (g1980 x) = f (g1979 x)
@[simp] axiom s1980 (x : Prop) : f (g1981 x) = f (g1980 x)
@[simp] axiom s1981 (x : Prop) : f (g1982 x) = f (g1981 x)
@[simp] axiom s1982 (x : Prop) : f (g1983 x) = f (g1982 x)
@[simp] axiom s1983 (x : Prop) : f (g1984 x) = f (g1983 x)
@[simp] axiom s1984 (x : Prop) : f (g1985 x) = f (g1984 x)
@[simp] axiom s1985 (x : Prop) : f (g1986 x) = f (g1985 x)
@[simp] axiom s1986 (x : Prop) : f (g1987 x) = f (g1986 x)
@[simp] axiom s1987 (x : Prop) : f (g1988 x) = f (g1987 x)
@[simp] axiom s1988 (x : Prop) : f (g1989 x) = f (g1988 x)
@[simp] axiom s1989 (x : Prop) : f (g1990 x) = f (g1989 x)
@[simp] axiom s1990 (x : Prop) : f (g1991 x) = f (g1990 x)
@[simp] axiom s1991 (x : Prop) : f (g1992 x) = f (g1991 x)
@[simp] axiom s1992 (x : Prop) : f (g1993 x) = f (g1992 x)
@[simp] axiom s1993 (x : Prop) : f (g1994 x) = f (g1993 x)
@[simp] axiom s1994 (x : Prop) : f (g1995 x) = f (g1994 x)
@[simp] axiom s1995 (x : Prop) : f (g1996 x) = f (g1995 x)
@[simp] axiom s1996 (x : Prop) : f (g1997 x) = f (g1996 x)
@[simp] axiom s1997 (x : Prop) : f (g1998 x) = f (g1997 x)
@[simp] axiom s1998 (x : Prop) : f (g1999 x) = f (g1998 x)