path: "vendor/opentheory/data/theories/parser-all-def/parser-all-def.art"
6 version "=" const 0 def "->" typeOp 1 def "bool" typeOp nil opType 2 def 1 ref 2 ref 2 ref nil cons 3 def cons opType 4 def nil cons cons opType 5 def constTerm 6 def refl 7 def "Data.Bool.!" const 8 def 1 ref 1 ref "Parser.parser" typeOp "A" varType 9 def "B" varType 10 def nil cons 11 def cons 12 def opType 13 def 3 ref cons opType 14 def 3 ref cons opType constTerm 15 def refl 16 def "p" 13 ref var 17 def "Data.Bool./\\" const 5 ref constTerm 18 def refl 19 def 17 ref 0 ref 1 ref "Parser.Stream.stream" typeOp 20 def 11 ref opType 21 def 1 ref 21 ref 3 ref cons opType nil cons cons opType constTerm 22 def "Parser.parse" "f" 1 ref 13 ref 1 ref 20 remove 9 ref nil cons 23 def opType 24 def 21 ref nil cons 25 def cons opType 26 def nil cons 27 def cons opType 28 def var 29 def nil cons cons nil cons 29 ref 15 ref 17 ref 18 ref 22 ref 29 ref varTerm 30 def 17 ref varTerm 31 def appTerm 32 def "Parser.Stream.error" const 33 def 24 ref constTerm 34 def appTerm appTerm 33 remove 21 ref constTerm 35 def appTerm appTerm 18 ref 22 ref 32 ref "Parser.Stream.eof" const 36 def 24 ref constTerm 37 def appTerm appTerm 36 remove 21 ref constTerm 38 def appTerm appTerm 8 ref 1 ref 1 ref 9 ref 3 ref cons opType 39 def 3 ref cons opType 40 def constTerm 41 def "x" 9 ref var 42 def 8 ref 1 ref 1 ref 24 ref 3 ref cons opType 43 def 3 ref cons opType 44 def constTerm 45 def "xs" 24 ref var 46 def 22 ref 32 ref "Parser.Stream.cons" const 47 def 1 ref 9 ref 1 ref 24 ref 24 ref nil cons 48 def cons opType nil cons cons opType constTerm 49 def 42 ref varTerm 50 def appTerm 51 def 46 ref varTerm 52 def appTerm 53 def appTerm appTerm "Data.Option.case.none.some" const 54 def 1 ref 21 ref 1 ref 1 ref "Data.Pair.*" typeOp 55 def 10 ref 48 ref cons opType 56 def 25 ref cons opType 57 def 1 ref "Data.Option.option" typeOp 58 def 56 ref nil cons 59 def opType 60 def 25 ref cons opType nil cons cons opType nil cons cons opType constTerm 35 ref appTerm 61 def "select" const 62 def 1 ref 1 ref 57 ref 3 ref cons opType 63 def 57 ref nil cons 64 def cons opType constTerm 65 def "f" 57 ref var 66 def 8 ref 1 ref 1 ref 10 ref 3 ref cons opType 67 def 3 ref cons opType 68 def constTerm 69 def "y" 10 ref var 70 def 45 ref "ys" 24 ref var 71 def 22 ref 66 ref varTerm "Data.Pair.," const 72 def 1 ref 10 ref 1 ref 24 ref 59 ref cons opType nil cons cons opType constTerm 73 def 70 ref varTerm 74 def appTerm 71 ref varTerm 75 def appTerm 76 def appTerm appTerm 77 def 47 remove 1 ref 10 ref 1 ref 21 ref 25 ref cons opType nil cons cons opType constTerm 78 def 74 ref appTerm 79 def 32 ref 75 ref appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm appTerm "Parser.dest" const 1 ref 13 ref 1 ref 9 ref 1 ref 24 ref 60 ref nil cons 80 def cons opType nil cons cons opType nil cons cons opType constTerm 31 ref appTerm 50 ref appTerm 81 def 52 ref appTerm 82 def appTerm appTerm absTerm appTerm absTerm appTerm appTerm appTerm absTerm appTerm absTerm 83 def refl 84 def 0 ref 1 ref 28 ref 1 ref 28 ref 3 ref cons opType 85 def nil cons cons opType constTerm 30 ref appTerm 62 ref 1 ref 85 ref 28 ref nil cons 86 def cons opType constTerm 87 def 83 ref appTerm appTerm assume sym appThm 83 ref 30 remove appTerm betaConv trans "A" 86 remove cons nil cons nil nil cons 88 def cons nil 0 ref 1 ref 40 ref 1 ref 40 ref 3 ref cons opType 89 def nil cons cons opType constTerm 90 def "Data.Bool.?" const 91 def 40 ref constTerm 92 def appTerm 93 def "p" 39 ref var 94 def 94 ref varTerm 95 def 62 ref 1 ref 39 ref 23 ref cons opType constTerm 95 ref appTerm appTerm 96 def absTerm appTerm axiom subst 84 remove appThm "p" 85 ref var 97 def 97 remove varTerm 98 def 87 remove 98 remove appTerm appTerm absTerm 83 remove appTerm betaConv trans 7 ref 16 ref 17 ref 91 ref 1 ref 1 ref 26 ref 3 ref cons opType 99 def 3 ref cons opType 100 def constTerm 101 def refl "f" 26 ref var 102 def 17 ref 102 ref 18 ref 22 ref 102 ref varTerm 103 def 34 ref appTerm appTerm 35 ref appTerm 104 def appTerm 18 ref 22 ref 103 ref 37 ref appTerm appTerm 38 ref appTerm 105 def appTerm 41 ref 42 ref 45 ref 46 ref 22 ref 103 ref 53 ref appTerm appTerm 61 ref 65 ref 66 ref 69 ref 70 ref 45 ref 71 ref 77 ref 79 ref 103 ref 75 ref appTerm 106 def appTerm 107 def appTerm absTerm appTerm absTerm appTerm absTerm appTerm 108 def appTerm 109 def 82 ref appTerm 110 def appTerm 111 def absTerm 112 def appTerm 113 def absTerm 114 def appTerm 115 def appTerm 116 def appTerm absTerm 117 def absTerm 118 def 31 ref appTerm betaConv 119 def 103 ref refl appThm 117 ref 103 ref appTerm betaConv 120 def trans absThm appThm absThm appThm appThm 91 ref 1 ref 85 remove 3 ref cons opType constTerm refl 29 remove 16 ref 17 ref 119 remove 32 ref refl appThm 117 ref 32 remove appTerm betaConv trans absThm appThm absThm appThm appThm nil "r" 1 ref 13 ref 99 ref nil cons 121 def cons opType var 118 remove nil cons cons nil cons nil cons cons "B" 27 ref cons "A" 13 ref nil cons cons nil cons 122 def cons 88 ref cons "r" 1 ref 9 ref 67 ref nil cons 123 def cons opType 124 def var 125 def 6 ref 41 ref 42 ref 91 ref 68 remove constTerm 126 def 70 ref 125 remove varTerm 127 def 50 ref appTerm 128 def 74 ref appTerm absTerm appTerm absTerm appTerm appTerm 91 ref 1 ref 1 ref 1 ref 12 ref opType 129 def 3 ref cons opType 130 def 3 ref cons opType 131 def constTerm "f" 129 ref var 132 def 41 ref 42 ref 128 remove 132 ref varTerm 133 def 50 ref appTerm appTerm absTerm appTerm absTerm appTerm appTerm absTerm 134 def 127 ref appTerm 135 def betaConv nil 8 ref 1 ref 1 ref 124 ref 3 ref cons opType 136 def 3 ref cons opType constTerm 134 ref appTerm 137 def axiom nil "p" 2 ref var 138 def 137 remove nil cons cons "q" 2 ref var 139 def 135 remove nil cons cons nil cons cons nil cons cons 6 ref "Data.Bool.==>" const 5 ref constTerm 140 def 138 ref varTerm 141 def appTerm 142 def 139 ref varTerm 143 def appTerm 144 def appTerm 145 def refl 138 ref 139 ref 6 ref 18 ref 141 ref appTerm 146 def 143 ref appTerm 147 def appTerm 148 def 141 ref appTerm absTerm 149 def absTerm 150 def 141 ref appTerm betaConv 143 ref refl 151 def appThm 149 remove 143 ref appTerm betaConv trans appThm nil 0 ref 1 ref 5 ref 1 ref 5 ref 3 ref cons opType 152 def nil cons cons opType constTerm 153 def 140 ref appTerm 150 remove appTerm axiom 141 ref refl 154 def appThm 151 ref appThm eqMp 155 def sym 156 def 148 remove refl 139 ref 0 ref 1 ref 152 ref 1 ref 152 remove 3 ref cons opType nil cons cons opType constTerm 157 def "f" 5 ref var 158 def 158 ref varTerm 159 def 141 ref appTerm 143 ref appTerm absTerm 160 def appTerm 158 ref 159 ref "Data.Bool.T" const 2 ref constTerm 161 def appTerm 161 ref appTerm absTerm 162 def appTerm absTerm 163 def 143 ref appTerm betaConv appThm 0 ref 1 ref 4 ref 1 ref 4 ref 3 ref cons opType 164 def nil cons cons opType constTerm 165 def 146 remove appTerm refl 138 ref 163 remove absTerm 166 def 141 ref appTerm betaConv appThm nil 153 ref 18 ref appTerm 166 ref appTerm axiom 167 def 154 remove appThm eqMp 151 ref appThm eqMp 168 def sym 158 ref 159 ref refl nil "t" 2 ref var 169 def 141 ref nil cons 170 def cons nil cons nil cons cons 6 ref 169 ref varTerm 171 def appTerm 161 ref appTerm assume sym nil 161 ref axiom 172 def eqMp 171 ref assume 172 ref deductAntisym deductAntisym 173 def subst 141 ref assume 174 def eqMp appThm nil 169 ref 143 ref nil cons 175 def cons nil cons nil cons cons 173 ref subst 143 ref assume 176 def eqMp appThm absThm eqMp 177 def nil "P" 2 ref var 178 def 170 ref cons "Q" 2 ref var 179 def 175 ref cons nil cons 180 def cons nil cons cons 7 ref 158 ref 159 remove 178 ref varTerm 181 def appTerm 182 def 179 ref varTerm 183 def appTerm absTerm 184 def 138 ref 139 ref 141 ref absTerm absTerm 185 def appTerm betaConv 185 ref 181 ref appTerm betaConv 183 ref refl 186 def appThm 139 ref 181 ref absTerm 183 ref appTerm betaConv trans trans appThm 162 ref 185 ref appTerm betaConv 185 ref 161 ref appTerm betaConv 161 ref refl 187 def appThm 139 ref 161 ref absTerm 161 ref appTerm betaConv trans trans appThm 6 ref 18 ref 181 ref appTerm 188 def 183 ref appTerm 189 def appTerm refl 139 ref 157 remove 158 remove 182 remove 143 ref appTerm absTerm appTerm 162 ref appTerm absTerm 183 ref appTerm betaConv appThm 165 ref 188 remove appTerm refl 166 remove 181 ref appTerm betaConv appThm 167 remove 181 ref refl 190 def appThm eqMp 186 ref appThm eqMp 189 remove assume eqMp 191 def 185 remove refl appThm eqMp sym 172 ref eqMp 192 def subst 193 def deductAntisym eqMp 155 remove 144 ref assume eqMp sym 174 ref eqMp 7 ref 160 remove 138 ref 139 ref 143 ref absTerm 194 def absTerm 195 def appTerm betaConv 195 ref 141 ref appTerm betaConv 151 remove appThm 194 ref 143 ref appTerm betaConv trans trans appThm 162 remove 195 ref appTerm betaConv 195 ref 161 ref appTerm betaConv 187 remove appThm 194 ref 161 ref appTerm betaConv trans trans 196 def appThm 168 remove 147 remove assume eqMp 195 ref refl 197 def appThm eqMp sym 172 ref eqMp 198 def proveHyp 199 def deductAntisym 200 def subst proveHyp "A" 124 ref nil cons cons nil cons "P" 136 remove var 134 remove nil cons cons "x" 124 remove var 127 remove nil cons cons nil cons cons nil cons cons nil 138 ref 41 ref "P" 39 ref var 201 def varTerm 202 def appTerm 203 def nil cons 204 def cons 139 ref 202 ref 50 ref appTerm 205 def nil cons 206 def cons nil cons cons nil cons cons 207 def 156 ref subst 207 remove 198 remove 177 remove deductAntisym 208 def subst 6 ref 205 ref appTerm refl 42 ref 161 ref absTerm 209 def 50 ref appTerm betaConv appThm 94 ref 0 ref 1 ref 39 ref 40 ref nil cons cons opType constTerm 95 ref appTerm 209 remove appTerm absTerm 210 def 202 ref appTerm betaConv 211 def nil 90 remove 41 ref appTerm 210 remove appTerm axiom 202 ref refl 212 def appThm 213 def 203 ref assume eqMp eqMp 50 ref refl 214 def appThm eqMp sym 172 ref eqMp eqMp nil 178 ref 204 remove cons 179 ref 206 ref cons nil cons cons nil cons cons 192 ref subst deductAntisym eqMp 215 def subst eqMp eqMp subst subst eqMp nil "P" 14 ref var 216 def 17 ref 101 ref 117 ref appTerm 217 def absTerm nil cons cons nil cons nil cons cons 122 ref 88 ref cons 218 def 6 ref 203 remove appTerm refl 211 remove appThm 213 remove eqMp sym 219 def subst subst 17 ref nil 169 ref 217 ref nil cons 220 def cons nil cons nil cons cons 173 ref subst nil "P" 99 remove var 221 def 102 ref 8 ref 100 remove constTerm 222 def "g" 26 ref var 223 def 45 ref 46 ref 140 ref 45 ref 71 ref 140 ref "Parser.Stream.isProperSuffix" const 1 ref 24 ref 43 ref nil cons cons opType 224 def constTerm 225 def 75 ref appTerm 226 def 52 ref appTerm 227 def appTerm 228 def 22 ref 106 remove appTerm 223 ref varTerm 229 def 75 ref appTerm 230 def appTerm 231 def appTerm absTerm 232 def appTerm 233 def appTerm 22 ref 223 ref "Parser.Stream.case.error.eof.cons" const 234 def 1 ref 21 ref 1 ref 21 ref 1 ref 1 ref 9 ref 27 ref cons opType 235 def 27 ref cons opType nil cons cons opType nil cons cons opType constTerm 35 ref appTerm 38 ref appTerm 42 ref "xt" 24 ref var 236 def 61 ref 65 ref 66 ref 69 ref 70 ref 45 ref 71 ref 77 ref 79 ref 230 remove appTerm 237 def appTerm absTerm appTerm absTerm appTerm absTerm appTerm 238 def appTerm 239 def 81 remove 236 ref varTerm 240 def appTerm 241 def appTerm 242 def absTerm 243 def absTerm 244 def appTerm absTerm 245 def 103 ref appTerm 246 def 52 ref appTerm 247 def appTerm 245 ref 229 ref appTerm 248 def 52 ref appTerm appTerm 249 def appTerm 250 def absTerm 251 def appTerm 252 def absTerm 253 def appTerm 254 def absTerm 255 def nil cons cons nil cons nil cons cons "A" 27 ref cons nil cons 256 def 88 ref cons 219 ref subst 257 def subst 102 ref nil 169 ref 254 remove nil cons cons nil cons nil cons cons 173 ref subst nil 221 ref 253 remove nil cons cons nil cons nil cons cons 257 ref subst 223 remove nil 169 ref 252 remove nil cons cons nil cons nil cons cons 173 ref subst nil "P" 43 remove var 258 def 251 remove nil cons cons nil cons nil cons cons "A" 48 ref cons nil cons 259 def 88 ref cons 219 ref subst 260 def subst 46 ref nil 169 ref 250 remove nil cons cons nil cons nil cons cons 173 ref subst nil 138 ref 233 remove nil cons 261 def cons 262 def 139 ref 249 ref nil cons 263 def cons nil cons 264 def cons nil cons cons 265 def 156 ref subst 265 remove 208 ref subst 46 ref "Data.Bool.\\/" const 5 remove constTerm 266 def 0 ref 224 ref constTerm 267 def 52 ref appTerm 268 def 34 ref appTerm 269 def appTerm 266 ref 268 ref 37 ref appTerm 270 def appTerm 92 ref 42 ref 91 ref 44 remove constTerm 271 def 236 ref 268 remove 51 remove 240 ref appTerm appTerm 272 def absTerm 273 def appTerm 274 def absTerm 275 def appTerm 276 def appTerm 277 def appTerm 278 def absTerm 279 def 52 ref appTerm 280 def betaConv nil 45 ref 279 ref appTerm 281 def axiom nil 138 ref 281 remove nil cons cons 139 ref 280 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 259 ref 258 ref 279 remove nil cons cons "x" 24 ref var 282 def 52 ref nil cons cons nil cons 283 def cons nil cons cons 215 ref subst eqMp eqMp nil 138 ref 278 remove nil cons 284 def cons 264 ref cons nil cons cons 285 def 200 ref subst proveHyp 285 ref 156 ref subst 285 remove 208 ref subst nil 138 ref 277 remove nil cons 286 def cons 264 ref cons nil cons cons 287 def 156 ref subst 287 remove 208 ref subst nil 201 ref 42 ref 140 ref 275 ref 50 ref appTerm 288 def appTerm 249 ref appTerm 289 def absTerm 290 def nil cons cons nil cons nil cons cons 219 ref subst 42 ref nil 169 ref 289 remove nil cons cons nil cons nil cons cons 173 ref subst nil 138 ref 288 ref nil cons 291 def cons 264 ref cons nil cons cons 292 def 156 ref subst 292 remove 208 ref subst 288 ref betaConv 288 remove assume eqMp nil 138 ref 274 ref nil cons cons 264 ref cons nil cons cons 200 ref subst proveHyp nil 258 ref 236 ref 140 ref 273 ref 240 ref appTerm 293 def appTerm 249 ref appTerm 294 def absTerm nil cons cons nil cons nil cons cons 260 ref subst 236 ref nil 169 ref 294 remove nil cons cons nil cons nil cons cons 173 ref subst nil 138 ref 293 ref nil cons 295 def cons 264 ref cons nil cons cons 296 def 156 ref subst 296 remove 208 ref subst 293 ref betaConv 293 remove assume eqMp nil 138 ref 272 ref nil cons 297 def cons 264 ref cons nil cons cons 298 def 200 ref subst proveHyp 298 ref 156 ref subst 298 remove 208 ref subst 22 ref refl 299 def 246 remove betaConv 300 def 272 remove assume 301 def appThm nil 46 ref 240 ref nil cons 302 def cons 303 def "f" 235 remove var 304 def 42 ref 236 remove 109 ref 241 ref appTerm 305 def absTerm 306 def absTerm 307 def nil cons cons "b" 21 ref var 308 def 38 ref nil cons 309 def cons "e" 21 ref var 35 ref nil cons 310 def cons nil cons cons 311 def cons 312 def cons nil cons cons "A" 23 ref cons 313 def "B" 25 ref cons nil cons 314 def cons 88 ref cons 315 def 46 ref 0 ref 1 ref 10 ref 123 remove cons opType constTerm 316 def 234 remove 1 ref 10 ref 1 ref 10 ref 1 ref 1 ref 9 ref 1 ref 24 ref 11 ref cons opType 317 def nil cons 318 def cons opType 319 def 318 ref cons opType nil cons cons opType nil cons cons opType constTerm "e" 10 ref var 320 def varTerm 321 def appTerm "b" 10 ref var 322 def varTerm 323 def appTerm "f" 319 ref var 324 def varTerm 325 def appTerm 326 def 53 ref appTerm appTerm 325 ref 50 ref appTerm 52 ref appTerm appTerm absTerm 327 def 52 ref appTerm 328 def betaConv 42 ref 45 ref 327 ref appTerm 329 def absTerm 330 def 50 ref appTerm 331 def betaConv 324 ref 41 ref 330 ref appTerm 332 def absTerm 333 def 325 ref appTerm 334 def betaConv 322 ref 8 ref 1 ref 1 ref 319 ref 3 ref cons opType 335 def 3 ref cons opType constTerm 336 def 333 ref appTerm 337 def absTerm 338 def 323 ref appTerm 339 def betaConv 320 ref 69 ref 338 ref appTerm 340 def absTerm 341 def 321 ref appTerm 342 def betaConv nil 18 ref 69 ref 320 ref 69 ref 322 ref 336 ref 324 ref 316 ref 326 ref 34 ref appTerm appTerm 321 ref appTerm absTerm 343 def appTerm 344 def absTerm 345 def appTerm 346 def absTerm 347 def appTerm 348 def appTerm 18 ref 69 ref 320 remove 69 ref 322 ref 336 remove 324 remove 316 ref 326 remove 37 ref appTerm appTerm 323 ref appTerm absTerm 349 def appTerm 350 def absTerm 351 def appTerm 352 def absTerm 353 def appTerm 354 def appTerm 69 ref 341 ref appTerm 355 def appTerm 356 def appTerm axiom 357 def nil 178 ref 348 remove nil cons 358 def cons 179 ref 356 remove nil cons cons nil cons cons nil cons cons 359 def 7 ref 184 remove 195 ref appTerm betaConv 195 remove 181 ref appTerm betaConv 186 ref appThm 194 remove 183 ref appTerm betaConv trans trans appThm 196 remove appThm 191 remove 197 remove appThm eqMp sym 172 ref eqMp 360 def subst proveHyp 361 def nil 178 ref 354 remove nil cons 362 def cons 179 ref 355 remove nil cons 363 def cons nil cons cons nil cons cons 364 def 360 ref subst proveHyp nil 138 ref 363 remove cons 139 ref 342 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp "A" 11 ref cons 365 def nil cons 366 def "P" 67 remove var 367 def 341 remove nil cons cons "x" 10 ref var 368 def 321 ref nil cons cons nil cons 369 def cons nil cons cons 215 ref subst eqMp eqMp nil 138 ref 340 remove nil cons cons 139 ref 339 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 366 ref 367 ref 338 remove nil cons cons 368 ref 323 ref nil cons cons nil cons 370 def cons nil cons cons 215 ref subst eqMp eqMp nil 138 ref 337 remove nil cons cons 139 ref 334 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp "A" 319 ref nil cons cons nil cons 371 def "P" 335 remove var 372 def 333 remove nil cons cons "x" 319 remove var 325 ref nil cons cons nil cons 373 def cons nil cons cons 215 ref subst eqMp eqMp nil 138 ref 332 remove nil cons cons 139 ref 331 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 313 ref nil cons 374 def 201 ref 330 remove nil cons cons 42 ref 50 ref nil cons 375 def cons nil cons 376 def cons nil cons cons 215 ref subst eqMp eqMp nil 138 ref 329 remove nil cons cons 139 ref 328 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 259 ref 258 ref 327 remove nil cons cons 283 ref cons nil cons cons 215 ref subst eqMp eqMp subst 377 def subst 307 remove 50 ref appTerm betaConv 378 def 240 ref refl 379 def appThm 306 ref 240 ref appTerm betaConv trans trans trans appThm 248 remove betaConv 380 def 301 ref appThm nil 303 remove 304 remove 244 ref nil cons cons 311 remove cons 381 def cons nil cons cons 377 ref subst 244 remove 50 ref appTerm betaConv 379 remove appThm 243 remove 240 ref appTerm betaConv trans trans trans appThm sym 46 ref 266 ref 0 ref 1 ref 60 ref 1 ref 60 ref 3 ref cons opType nil cons cons opType constTerm 382 def 82 ref appTerm 383 def "Data.Option.none" const 384 def 60 remove constTerm 385 def appTerm appTerm 126 ref 70 ref 271 ref 71 ref 18 ref 383 remove "Data.Option.some" const 386 def 1 ref 56 ref 80 remove cons opType constTerm 76 ref appTerm 387 def appTerm appTerm "Parser.Stream.isSuffix" const 224 remove constTerm 388 def 75 ref appTerm 389 def 52 ref appTerm appTerm absTerm appTerm absTerm appTerm appTerm absTerm 390 def 240 ref appTerm 391 def betaConv 42 ref 45 ref 390 ref appTerm 392 def absTerm 393 def 50 ref appTerm 394 def betaConv 17 ref 41 ref 393 ref appTerm 395 def absTerm 396 def 31 ref appTerm 397 def betaConv nil 15 ref 396 ref appTerm 398 def axiom nil 138 ref 398 remove nil cons cons 139 ref 397 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 122 remove 216 remove 396 remove nil cons cons "x" 13 remove var 31 ref nil cons cons nil cons cons nil cons cons 215 ref subst eqMp eqMp nil 138 ref 395 remove nil cons cons 139 ref 394 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 374 ref 201 ref 393 remove nil cons cons 376 ref cons nil cons cons 215 ref subst eqMp eqMp nil 138 ref 392 remove nil cons cons 139 ref 391 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 259 ref 258 ref 390 remove nil cons cons 282 ref 302 ref cons nil cons cons nil cons cons 215 ref subst eqMp eqMp nil 138 ref 266 ref 382 remove 241 remove appTerm 399 def 385 remove appTerm 400 def appTerm 126 remove 70 ref 271 remove 71 ref 18 ref 399 remove 387 remove appTerm 401 def appTerm 389 remove 240 remove appTerm 402 def appTerm 403 def absTerm 404 def appTerm 405 def absTerm 406 def appTerm 407 def appTerm nil cons 408 def cons 139 ref 22 ref 305 remove appTerm 242 remove appTerm 409 def nil cons 410 def cons nil cons 411 def cons nil cons cons 412 def 200 ref subst proveHyp 412 ref 156 ref subst 412 remove 208 ref subst nil 367 ref 70 ref 140 ref 406 ref 74 ref appTerm 413 def appTerm 409 ref appTerm 414 def absTerm nil cons cons nil cons nil cons cons 366 ref 88 ref cons 219 ref subst 415 def subst 70 ref nil 169 ref 414 remove nil cons cons nil cons nil cons cons 173 ref subst nil 138 ref 413 ref nil cons 416 def cons 411 ref cons nil cons cons 417 def 156 ref subst 417 remove 208 ref subst 413 ref betaConv 413 remove assume eqMp nil 138 ref 405 ref nil cons cons 411 ref cons nil cons cons 200 ref subst proveHyp nil 258 ref 71 ref 140 ref 404 ref 75 ref appTerm 418 def appTerm 409 ref appTerm 419 def absTerm nil cons cons nil cons nil cons cons 260 ref subst 71 ref nil 169 ref 419 remove nil cons cons nil cons nil cons cons 173 ref subst nil 138 ref 418 ref nil cons 420 def cons 411 ref cons nil cons cons 421 def 156 ref subst 421 remove 208 ref subst 418 ref betaConv 418 remove assume eqMp nil 138 ref 403 remove nil cons 422 def cons 411 ref cons nil cons cons 423 def 200 ref subst proveHyp 423 ref 156 ref subst 423 remove 208 ref subst nil 178 ref 401 ref nil cons cons 179 ref 402 ref nil cons 424 def cons nil cons cons nil cons cons 425 def 192 ref subst 425 remove 360 ref subst 299 ref 109 remove refl 426 def 401 remove assume 427 def appThm nil "a" 56 ref var 76 ref nil cons cons 428 def 66 ref 108 remove nil cons cons 308 remove 310 ref cons nil cons 429 def cons 430 def cons nil cons cons "A" 59 remove cons 314 remove cons 88 ref cons 431 def "a" 9 ref var 432 def 316 ref 54 remove 1 ref 10 ref 1 ref 129 ref 1 ref 58 remove 23 ref opType 433 def 11 ref cons opType nil cons cons opType nil cons cons opType constTerm 323 ref appTerm 133 ref appTerm 434 def 386 remove 1 ref 9 ref 433 ref nil cons cons opType constTerm 432 ref varTerm 435 def appTerm appTerm appTerm 133 ref 435 ref appTerm appTerm absTerm 436 def 435 ref appTerm 437 def betaConv 132 ref 41 ref 436 ref appTerm 438 def absTerm 439 def 133 ref appTerm 440 def betaConv 322 ref 8 ref 131 remove constTerm 441 def 439 ref appTerm 442 def absTerm 443 def 323 ref appTerm 444 def betaConv nil 69 ref 443 ref appTerm 445 def axiom nil 138 ref 445 remove nil cons cons 139 ref 444 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 366 ref 367 ref 443 remove nil cons cons 370 ref cons nil cons cons 215 ref subst eqMp eqMp nil 138 ref 442 remove nil cons cons 139 ref 440 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp "A" 129 ref nil cons cons nil cons 446 def "P" 130 ref var 447 def 439 remove nil cons cons "x" 129 ref var 448 def 133 ref nil cons cons nil cons 449 def cons nil cons cons 215 ref subst eqMp eqMp nil 138 ref 438 remove nil cons cons 139 ref 437 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 374 ref 201 ref 436 remove nil cons cons 42 ref 435 ref nil cons cons nil cons 450 def cons nil cons cons 215 ref subst eqMp eqMp subst 451 def subst 71 ref 22 ref 65 ref "_31778" 57 ref var 452 def 69 ref 70 ref 45 ref 71 ref 22 ref 452 remove varTerm 76 ref appTerm appTerm 107 ref appTerm absTerm appTerm absTerm appTerm absTerm 453 def appTerm 454 def 76 ref appTerm appTerm 107 ref appTerm absTerm 455 def 75 ref appTerm 456 def betaConv 70 ref 45 ref 455 ref appTerm 457 def absTerm 458 def 74 ref appTerm 459 def betaConv 453 ref 454 remove appTerm 460 def betaConv 453 ref "_31776" 56 ref var 461 def 78 ref 62 ref 1 ref 1 ref 1 ref 56 ref 11 ref cons opType 462 def 3 ref cons opType 462 ref nil cons cons opType constTerm "fn" 462 remove var 463 def 69 ref "a" 10 ref var 464 def 45 ref "b" 24 ref var 465 def 316 ref 463 remove varTerm 73 remove 464 ref varTerm 466 def appTerm 465 ref varTerm 467 def appTerm 468 def appTerm appTerm 466 remove appTerm absTerm appTerm absTerm appTerm absTerm appTerm 469 def 461 remove varTerm 470 def appTerm appTerm 103 ref 62 ref 1 ref 1 ref 1 ref 56 ref 48 ref cons opType 471 def 3 ref cons opType 471 ref nil cons cons opType constTerm "fn" 471 remove var 472 def 69 ref 464 ref 45 ref 465 ref 267 remove 472 remove varTerm 468 remove appTerm appTerm 467 remove appTerm absTerm appTerm absTerm appTerm absTerm appTerm 473 def 470 remove appTerm appTerm appTerm absTerm 474 def appTerm betaConv sym nil 367 ref 70 ref 45 ref 71 ref 22 ref 474 ref 76 ref appTerm 475 def appTerm 107 remove appTerm 476 def absTerm 477 def appTerm 478 def absTerm nil cons cons nil cons nil cons cons 415 ref subst 70 ref nil 169 ref 478 remove nil cons cons nil cons nil cons cons 173 ref subst nil 258 ref 477 remove nil cons cons nil cons nil cons cons 260 ref subst 71 ref nil 169 ref 476 remove nil cons cons nil cons nil cons cons 173 ref subst 475 remove betaConv 22 ref "_31773" 24 ref var 479 def 79 ref 103 ref 479 ref varTerm appTerm 480 def appTerm absTerm 75 ref appTerm 481 def appTerm refl 479 ref 78 ref 469 ref 76 ref appTerm 482 def appTerm 483 def 480 ref appTerm absTerm 484 def 473 ref 76 ref appTerm 485 def appTerm betaConv appThm 299 ref 481 remove betaConv appThm 483 ref 103 ref 485 ref appTerm appTerm refl appThm trans 0 ref 1 ref 26 ref 121 remove cons opType constTerm 486 def "_31772" 10 ref var 487 def 479 remove 78 ref 487 remove varTerm appTerm 480 remove appTerm absTerm absTerm 488 def 74 ref appTerm 489 def appTerm refl 488 ref 482 ref appTerm betaConv appThm 486 ref refl 490 def 489 remove betaConv appThm 484 remove refl appThm trans 488 remove refl nil 465 remove 75 ref nil cons 491 def cons 464 remove 74 ref nil cons 492 def cons nil cons cons nil cons cons 493 def 365 remove "B" 48 remove cons nil cons cons 88 ref cons 494 def 322 ref 0 ref 1 ref 9 ref 39 ref nil cons 495 def cons opType constTerm 496 def 62 ref 1 ref 1 ref 1 ref 55 remove 12 remove opType 497 def 23 ref cons opType 498 def 3 ref cons opType 499 def 498 ref nil cons 500 def cons opType constTerm "fn" 498 remove var 501 def 41 ref 432 ref 69 ref 322 ref 496 ref 501 ref varTerm 72 remove 1 ref 9 ref 1 ref 10 ref 497 ref nil cons cons opType nil cons cons opType constTerm 435 ref appTerm 323 ref appTerm 502 def appTerm appTerm 503 def 435 ref appTerm absTerm appTerm absTerm appTerm absTerm 504 def appTerm 505 def 502 ref appTerm appTerm 435 ref appTerm absTerm 506 def 323 ref appTerm 507 def betaConv 432 ref 69 ref 506 ref appTerm 508 def absTerm 509 def 435 ref appTerm 510 def betaConv 504 ref 505 remove appTerm 511 def betaConv 91 ref 1 ref 499 ref 3 ref cons opType constTerm 512 def refl 501 remove 41 ref refl 513 def 432 ref 69 ref refl 514 def 322 ref 503 remove refl 432 ref 322 ref 435 ref absTerm 515 def absTerm 516 def 435 ref appTerm betaConv 323 ref refl 517 def appThm 515 remove 323 ref appTerm betaConv trans appThm absThm appThm absThm appThm absThm appThm "C" 23 ref cons nil cons "_1343" 1 ref 9 ref 1 ref 10 ref 23 remove cons opType nil cons cons opType var 516 remove nil cons cons nil cons nil cons cons nil "f" 1 ref 9 ref 1 ref 10 ref "C" varType 518 def nil cons 519 def cons opType nil cons cons opType 520 def var 521 def 432 ref 322 ref "_1343" 520 ref var varTerm 435 ref appTerm 323 ref appTerm 522 def absTerm 523 def absTerm 524 def nil cons cons nil cons nil cons cons 521 ref 91 ref 1 ref 1 ref 1 ref 497 ref 519 remove cons opType 525 def 3 ref cons opType 526 def 3 ref cons opType 527 def constTerm 528 def "fn" 525 ref var 529 def 41 ref 432 ref 69 ref 322 ref 0 ref 1 ref 518 ref 1 ref 518 remove 3 ref cons opType nil cons cons opType constTerm 529 ref varTerm 530 def 502 ref appTerm appTerm 531 def 521 remove varTerm 532 def 435 ref appTerm 323 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 533 def 532 ref appTerm 534 def betaConv nil 8 ref 1 ref 1 ref 520 ref 3 ref cons opType 535 def 3 ref cons opType constTerm 533 ref appTerm 536 def axiom nil 138 ref 536 remove nil cons cons 139 ref 534 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp "A" 520 ref nil cons cons nil cons "P" 535 remove var 533 remove nil cons cons "x" 520 remove var 532 remove nil cons cons nil cons cons nil cons cons 215 ref subst eqMp eqMp subst nil 138 ref 528 ref 529 ref 41 ref 432 ref 69 ref 322 ref 531 ref 524 remove 435 ref appTerm 537 def 323 ref appTerm appTerm absTerm appTerm absTerm appTerm 538 def absTerm 539 def appTerm 540 def nil cons cons 139 ref 528 remove 529 ref 41 ref 432 ref 69 ref 322 ref 531 ref 522 remove appTerm absTerm appTerm absTerm appTerm absTerm 541 def appTerm 542 def nil cons 543 def cons nil cons 544 def cons nil cons cons 200 ref subst nil "P" 526 remove var 545 def 529 ref 140 ref 539 ref 530 ref appTerm 546 def appTerm 542 ref appTerm 547 def absTerm nil cons cons nil cons nil cons cons "A" 525 ref nil cons cons nil cons 548 def 88 ref cons 219 ref subst subst 529 remove nil 169 ref 547 remove nil cons cons nil cons nil cons cons 173 ref subst nil 138 ref 546 ref nil cons 549 def cons 544 ref cons nil cons cons 550 def 156 ref subst 550 remove 208 ref subst 546 ref betaConv 546 remove assume eqMp nil 138 ref 538 ref nil cons 551 def cons 544 remove cons nil cons cons 552 def 200 ref subst proveHyp 552 ref 156 ref subst 552 remove 208 ref subst 541 ref 530 ref appTerm betaConv sym 513 ref 432 ref 514 ref 322 ref 531 remove refl 537 remove betaConv 517 ref appThm 523 remove 323 ref appTerm betaConv trans appThm absThm appThm absThm appThm 538 remove assume eqMp eqMp 548 ref 545 ref 541 remove nil cons cons "x" 525 remove var 553 def 530 remove nil cons cons nil cons cons nil cons cons 6 ref 92 ref 202 ref appTerm 554 def appTerm 555 def refl 94 ref 8 ref 164 remove constTerm 556 def 139 ref 140 ref 41 ref 42 ref 140 ref 95 ref 50 ref appTerm 557 def appTerm 558 def 143 ref appTerm absTerm appTerm appTerm 143 ref appTerm absTerm appTerm absTerm 559 def 202 remove appTerm betaConv appThm nil 93 remove 559 remove appTerm axiom 212 remove appThm eqMp 560 def sym nil "P" 4 remove var 561 def 179 ref 140 ref 41 ref 42 ref 140 ref 205 ref appTerm 562 def 183 ref appTerm 563 def absTerm 564 def appTerm 565 def appTerm 566 def 183 ref appTerm 567 def absTerm nil cons cons nil cons nil cons cons "A" 3 ref cons nil cons 568 def 88 ref cons 219 ref subst 569 def subst 179 ref nil 169 ref 567 remove nil cons cons nil cons nil cons cons 173 ref subst nil 138 ref 565 ref nil cons 570 def cons 571 def 139 ref 183 ref nil cons 572 def cons nil cons 573 def cons nil cons cons 574 def 156 ref subst 574 ref 208 ref subst nil 138 ref 206 ref cons 573 ref cons nil cons cons 575 def 200 ref subst 576 def 564 ref 50 ref appTerm 577 def betaConv nil 571 ref 139 ref 577 remove nil cons cons nil cons cons nil cons cons 200 ref subst 374 ref 201 ref 564 remove nil cons cons 578 def 376 ref cons nil cons cons 215 ref subst eqMp eqMp 579 def eqMp eqMp nil 178 ref 570 ref cons 580 def 179 ref 572 ref cons nil cons 581 def cons nil cons cons 192 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp 582 def subst proveHyp eqMp nil 178 ref 551 remove cons 179 ref 543 remove cons nil cons 583 def cons nil cons cons 192 ref subst deductAntisym eqMp eqMp eqMp nil 178 ref 549 remove cons 583 ref cons nil cons cons 192 ref subst deductAntisym eqMp eqMp absThm eqMp nil 138 ref 8 ref 527 remove constTerm 553 ref 140 ref 539 ref 553 remove varTerm appTerm appTerm 542 ref appTerm absTerm appTerm nil cons cons 139 ref 140 ref 540 remove appTerm 542 remove appTerm nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 548 remove 545 remove 539 remove nil cons cons 583 remove cons nil cons cons nil 571 ref 139 ref 140 ref 554 ref appTerm 584 def 183 ref appTerm nil cons 585 def cons nil cons cons nil cons cons 586 def 156 ref subst 586 remove 208 ref subst nil 138 ref 554 remove nil cons 587 def cons 588 def 573 ref cons nil cons cons 589 def 156 ref subst 589 remove 208 ref subst 574 remove 200 ref subst 139 ref 140 ref 41 ref 42 ref 562 remove 143 ref appTerm absTerm appTerm appTerm 143 ref appTerm absTerm 590 def 183 ref appTerm 591 def betaConv nil 588 remove 139 ref 556 ref 590 ref appTerm 592 def nil cons 593 def cons nil cons cons nil cons cons 594 def 200 ref subst 560 remove nil 138 ref 555 remove 592 ref appTerm nil cons cons 139 ref 584 remove 592 remove appTerm nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 594 remove nil 138 ref 6 ref 141 ref appTerm 595 def 143 ref appTerm 596 def nil cons 597 def cons 598 def 139 ref 144 ref nil cons 599 def cons nil cons 600 def cons nil cons cons 601 def 156 ref subst 601 remove 208 ref subst 156 ref 208 ref 596 remove assume 602 def 174 remove eqMp eqMp 193 ref deductAntisym eqMp 603 def eqMp nil 178 ref 597 remove cons 604 def 179 ref 599 ref cons nil cons 605 def cons nil cons cons 192 ref subst deductAntisym eqMp 606 def subst eqMp eqMp nil 138 ref 593 remove cons 139 ref 591 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 568 ref 561 ref 590 remove nil cons cons "x" 2 ref var 607 def 572 remove cons nil cons cons nil cons cons 215 ref subst eqMp eqMp eqMp eqMp nil 178 ref 587 remove cons 581 ref cons nil cons cons 192 ref subst deductAntisym eqMp eqMp nil 580 ref 179 ref 585 remove cons nil cons cons nil cons cons 192 ref subst deductAntisym eqMp 608 def subst eqMp eqMp proveHyp 609 def subst eqMp nil 138 ref 512 remove 504 ref appTerm nil cons cons 139 ref 511 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp "A" 500 remove cons nil cons "p" 499 remove var 504 remove nil cons cons nil cons nil cons cons nil 138 ref 92 ref 95 ref appTerm 610 def nil cons 611 def cons 612 def 139 ref 6 ref 96 ref appTerm 613 def 161 ref appTerm 614 def nil cons 615 def cons nil cons 616 def cons nil cons cons 617 def 156 ref subst 617 remove 208 ref subst 92 ref refl nil "t" 39 ref var 95 ref nil cons 618 def cons nil cons nil cons cons 313 remove "B" 3 ref cons nil cons cons 88 ref cons "t" 129 ref var 619 def 0 remove 1 ref 129 remove 130 remove nil cons cons opType constTerm 42 ref 619 remove varTerm 620 def 50 ref appTerm absTerm appTerm 620 ref appTerm absTerm 621 def 620 ref appTerm 622 def betaConv nil 441 ref 621 ref appTerm 623 def axiom nil 138 ref 623 remove nil cons cons 139 ref 622 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 446 ref 447 ref 621 remove nil cons cons 448 remove 620 remove nil cons cons nil cons cons nil cons cons 215 ref subst eqMp eqMp subst subst appThm nil 169 ref 611 ref cons nil cons nil cons cons 624 def 173 ref subst 610 ref assume eqMp trans sym 172 ref eqMp nil 138 ref 92 ref 42 ref 557 ref absTerm 625 def appTerm nil cons cons 616 ref cons nil cons cons 200 ref subst proveHyp nil 201 ref 618 ref cons 179 ref 615 remove cons nil cons 626 def cons nil cons cons nil 571 remove 139 ref 140 ref 92 remove 42 ref 205 ref absTerm 627 def appTerm 628 def appTerm 183 ref appTerm 629 def nil cons 630 def cons nil cons 631 def cons nil cons cons 632 def 603 remove nil 138 ref 599 ref cons 633 def 139 ref 140 ref 143 ref appTerm 634 def 141 ref appTerm nil cons 635 def cons nil cons 636 def cons nil cons cons 208 ref subst proveHyp 634 ref refl 602 remove appThm sym nil 138 ref 175 ref cons 637 def 139 ref 175 ref cons nil cons 638 def cons nil cons cons 639 def 156 ref subst 639 remove 208 ref subst 176 remove eqMp nil 178 ref 175 remove cons 180 ref cons nil cons cons 192 ref subst deductAntisym eqMp eqMp 640 def eqMp nil 637 ref 139 ref 170 ref cons nil cons 641 def cons nil cons cons 200 ref subst nil 178 ref 599 remove cons 642 def 179 ref 635 remove cons nil cons 643 def cons nil cons cons 644 def 360 ref subst eqMp 200 ref 644 remove 192 ref subst eqMp deductAntisym deductAntisym 645 def subst 632 ref 156 ref subst 632 remove 208 ref subst nil 201 ref 42 ref 140 ref 627 ref 50 ref appTerm 646 def appTerm 183 ref appTerm 647 def absTerm 648 def nil cons cons nil cons nil cons cons 219 ref subst 42 ref nil 169 ref 647 remove nil cons cons nil cons nil cons cons 173 ref subst nil 138 ref 646 ref nil cons 649 def cons 573 ref cons nil cons cons 650 def 156 ref subst 650 remove 208 ref subst 646 ref betaConv 651 def 646 remove assume eqMp 576 remove proveHyp 579 remove eqMp eqMp nil 178 ref 649 remove cons 581 ref cons nil cons cons 192 ref subst deductAntisym eqMp eqMp absThm eqMp nil 138 ref 41 ref 648 remove appTerm nil cons cons 631 remove cons nil cons cons 200 ref subst proveHyp 374 ref 201 ref 627 remove nil cons cons 652 def 581 ref cons nil cons cons 608 ref subst eqMp eqMp nil 580 remove 179 ref 630 ref cons nil cons cons nil cons cons 192 ref subst deductAntisym eqMp nil 138 ref 566 remove 629 ref appTerm nil cons cons 139 ref 140 ref 629 ref appTerm 565 remove appTerm nil cons cons nil cons cons nil cons cons 208 ref subst proveHyp nil 138 ref 630 ref cons 139 ref 570 ref cons nil cons cons nil cons cons 653 def 156 ref subst 653 remove 208 ref subst nil 578 remove nil cons nil cons cons 219 ref subst 42 ref nil 169 ref 563 remove nil cons cons nil cons nil cons cons 173 ref subst 575 ref 156 ref subst 575 remove 208 ref subst 651 remove sym 205 remove assume eqMp 374 ref 652 remove 376 ref cons nil cons cons 582 ref subst proveHyp nil 138 ref 628 remove nil cons cons 573 remove cons nil cons cons 200 ref subst 629 remove assume eqMp proveHyp eqMp nil 178 ref 206 remove cons 581 remove cons nil cons cons 192 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp nil 178 ref 630 remove cons 179 ref 570 remove cons nil cons cons nil cons cons 192 ref subst deductAntisym eqMp eqMp eqMp subst nil 201 ref 42 ref 558 ref 614 ref appTerm 654 def absTerm nil cons cons nil cons nil cons cons 219 ref subst 42 ref nil 169 ref 654 remove nil cons cons nil cons nil cons cons 173 ref subst nil 138 ref 557 ref nil cons 655 def cons 656 def 616 remove cons nil cons cons 657 def 156 ref subst 657 remove 208 ref subst nil 169 ref 96 ref nil cons 658 def cons nil cons nil cons cons 173 ref subst nil 656 remove 139 ref 658 remove cons 659 def nil cons cons nil cons cons 200 ref subst 42 ref 558 remove 96 ref appTerm absTerm 660 def 50 ref appTerm 661 def betaConv 94 ref 41 ref 660 ref appTerm 662 def absTerm 663 def 95 ref appTerm 664 def betaConv nil 8 ref 89 remove constTerm 665 def 663 ref appTerm 666 def axiom nil 138 ref 666 remove nil cons cons 139 ref 664 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp "A" 495 remove cons nil cons 667 def "P" 40 remove var 668 def 663 remove nil cons cons "x" 39 ref var 669 def 618 remove cons nil cons 670 def cons nil cons cons 215 ref subst eqMp eqMp nil 138 ref 662 remove nil cons cons 139 ref 661 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 374 ref 201 ref 660 remove nil cons cons 376 remove cons nil cons cons 215 ref subst eqMp eqMp eqMp eqMp eqMp nil 178 ref 655 remove cons 626 ref cons nil cons cons 192 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp eqMp eqMp nil 178 ref 611 ref cons 626 remove cons nil cons cons 192 ref subst deductAntisym eqMp nil 138 ref 140 ref 610 ref appTerm 671 def 614 remove appTerm nil cons cons 139 ref 6 ref 671 ref 96 remove appTerm appTerm 672 def 671 ref 161 ref appTerm appTerm nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp nil "q'" 2 ref var 673 def 161 ref nil cons cons nil cons nil cons cons 610 ref refl nil 138 ref 6 ref 610 ref appTerm 674 def 610 remove appTerm nil cons cons 139 ref 140 ref 671 ref 613 remove 673 ref varTerm 675 def appTerm 676 def appTerm appTerm 672 ref 671 remove 675 ref appTerm appTerm appTerm nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp nil "p'" 2 ref var 677 def 611 remove cons nil cons nil cons cons 673 ref 140 ref 674 remove 677 ref varTerm 678 def appTerm appTerm 140 ref 140 ref 678 ref appTerm 679 def 676 remove appTerm appTerm 672 remove 679 ref 675 ref appTerm 680 def appTerm appTerm appTerm absTerm 681 def 675 ref appTerm 682 def betaConv 677 ref 556 ref 681 ref appTerm 683 def absTerm 684 def 678 ref appTerm 685 def betaConv nil 659 remove 612 remove nil cons cons nil cons cons nil 561 ref 677 ref 556 ref 673 ref 140 ref 595 remove 678 ref appTerm 686 def appTerm 140 ref 679 ref 6 ref 143 ref appTerm 675 ref appTerm 687 def appTerm 688 def appTerm 145 remove 680 ref appTerm 689 def appTerm 690 def appTerm 691 def absTerm 692 def appTerm 693 def absTerm nil cons cons nil cons nil cons cons 569 ref subst 677 remove nil 169 ref 693 remove nil cons cons nil cons nil cons cons 173 ref subst nil 561 ref 692 remove nil cons cons nil cons nil cons cons 569 remove subst 673 remove nil 169 ref 691 remove nil cons cons nil cons nil cons cons 173 ref subst nil 138 ref 686 remove nil cons 694 def cons 695 def 139 ref 690 remove nil cons 696 def cons nil cons cons nil cons cons 697 def 156 ref subst 697 remove 208 ref subst nil 138 ref 688 ref nil cons 698 def cons 139 ref 689 remove nil cons 699 def cons nil cons cons nil cons cons 700 def 156 ref subst 700 remove 208 ref subst nil 633 remove 139 ref 680 ref nil cons 701 def cons nil cons cons nil cons cons 702 def 645 remove subst 702 ref 156 ref subst 702 remove 208 ref subst nil 138 ref 678 ref nil cons 703 def cons 704 def 139 ref 675 ref nil cons 705 def cons nil cons 706 def cons nil cons cons 707 def 156 ref subst 707 ref 208 ref subst nil 695 ref 139 ref 142 ref 678 remove appTerm 708 def nil cons 709 def cons nil cons cons nil cons cons 200 ref subst nil 138 ref 170 remove cons 139 ref 703 ref cons nil cons cons nil cons cons 710 def 606 ref subst eqMp 711 def nil 138 ref 709 ref cons 712 def 706 ref cons nil cons cons 713 def 200 ref subst proveHyp nil 695 remove 139 ref 679 remove 141 remove appTerm 714 def nil cons 715 def cons nil cons cons nil cons cons 200 ref subst 710 ref nil 598 remove 636 remove cons nil cons cons 716 def 156 ref subst 716 remove 208 ref subst 640 remove eqMp nil 604 remove 643 remove cons nil cons cons 192 ref subst deductAntisym eqMp 717 def subst eqMp 718 def nil 138 ref 715 ref cons 719 def 139 ref 140 ref 708 ref appTerm 720 def 675 ref appTerm nil cons 721 def cons nil cons cons nil cons cons 722 def 200 ref subst proveHyp 722 ref 156 ref subst 722 remove 208 ref subst 713 ref 156 ref subst 713 remove 208 ref subst nil 704 ref 641 remove cons nil cons cons 200 ref subst 714 remove assume eqMp 723 def 710 remove 200 ref subst 708 remove assume eqMp 724 def 723 remove proveHyp proveHyp nil 704 remove 139 ref 687 remove nil cons 725 def cons nil cons cons nil cons cons 200 ref subst 688 remove assume eqMp 726 def nil 138 ref 725 remove cons 727 def 139 ref 634 ref 675 ref appTerm 728 def nil cons 729 def cons nil cons cons nil cons cons 200 ref subst proveHyp nil 637 remove 706 ref cons nil cons cons 730 def 606 remove subst eqMp 731 def nil 138 ref 729 ref cons 732 def 706 remove cons nil cons cons 733 def 200 ref subst proveHyp 726 remove nil 727 remove 139 ref 140 ref 675 ref appTerm 143 ref appTerm 734 def nil cons 735 def cons nil cons cons nil cons cons 200 ref subst proveHyp 730 ref 717 remove subst eqMp 736 def nil 138 ref 735 ref cons 737 def 139 ref 140 ref 728 ref appTerm 738 def 675 remove appTerm nil cons 739 def cons nil cons cons nil cons cons 740 def 200 ref subst proveHyp 740 ref 156 ref subst 740 remove 208 ref subst 733 ref 156 ref subst 733 remove 208 ref subst 199 remove 730 remove 200 ref subst 728 remove assume eqMp proveHyp eqMp nil 178 ref 729 remove cons 741 def 179 ref 705 ref cons nil cons 742 def cons nil cons cons 192 ref subst deductAntisym eqMp eqMp nil 178 ref 735 remove cons 743 def 179 ref 739 remove cons nil cons cons nil cons cons 192 ref subst deductAntisym eqMp eqMp eqMp proveHyp eqMp nil 178 ref 709 remove cons 744 def 742 ref cons nil cons cons 192 ref subst deductAntisym eqMp eqMp nil 178 ref 715 remove cons 745 def 179 ref 721 remove cons nil cons cons nil cons cons 192 ref subst deductAntisym eqMp eqMp eqMp eqMp nil 178 ref 703 ref cons 742 remove cons nil cons cons 192 ref subst deductAntisym eqMp eqMp nil 642 remove 179 ref 701 ref cons nil cons cons nil cons cons 192 ref subst deductAntisym eqMp nil 138 ref 140 ref 144 ref appTerm 680 ref appTerm nil cons cons 139 ref 140 ref 680 ref appTerm 144 remove appTerm nil cons cons nil cons cons nil cons cons 208 ref subst proveHyp nil 138 ref 701 ref cons 600 remove cons nil cons cons 746 def 156 ref subst 746 remove 208 ref subst 156 ref 208 ref 711 remove nil 712 remove 638 ref cons nil cons cons 747 def 200 ref subst proveHyp 718 remove nil 719 remove 139 ref 720 remove 143 ref appTerm nil cons 748 def cons nil cons cons nil cons cons 749 def 200 ref subst proveHyp 749 ref 156 ref subst 749 remove 208 ref subst 747 ref 156 ref subst 747 remove 208 ref subst 724 remove 731 remove nil 732 remove 638 ref cons nil cons cons 750 def 200 ref subst proveHyp 736 remove nil 737 remove 139 ref 738 remove 143 remove appTerm nil cons 751 def cons nil cons cons nil cons cons 752 def 200 ref subst proveHyp 752 ref 156 ref subst 752 remove 208 ref subst 750 ref 156 ref subst 750 remove 208 ref subst 707 remove 200 ref subst 680 remove assume eqMp nil 138 ref 705 ref cons 638 remove cons nil cons cons 200 ref subst 734 remove assume eqMp proveHyp eqMp nil 741 remove 180 ref cons nil cons cons 192 ref subst deductAntisym eqMp eqMp nil 743 remove 179 ref 751 remove cons nil cons cons nil cons cons 192 ref subst deductAntisym eqMp eqMp eqMp proveHyp eqMp nil 744 remove 180 remove cons nil cons cons 192 ref subst deductAntisym eqMp eqMp nil 745 remove 179 ref 748 remove cons nil cons cons nil cons cons 192 ref subst deductAntisym eqMp eqMp eqMp eqMp 193 remove deductAntisym eqMp eqMp nil 178 ref 701 remove cons 605 remove cons nil cons cons 192 ref subst deductAntisym eqMp eqMp eqMp eqMp nil 178 ref 698 remove cons 179 ref 699 remove cons nil cons cons nil cons cons 192 ref subst deductAntisym eqMp eqMp nil 178 ref 694 remove cons 179 ref 696 remove cons nil cons cons nil cons cons 192 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp absThm eqMp subst nil 138 ref 556 ref 684 ref appTerm nil cons cons 139 ref 685 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 568 ref 561 ref 684 remove nil cons cons 607 ref 703 remove cons nil cons cons nil cons cons 215 ref subst eqMp eqMp nil 138 ref 683 remove nil cons cons 139 ref 682 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 568 ref 561 ref 681 remove nil cons cons 607 ref 705 remove cons nil cons cons nil cons cons 215 ref subst eqMp eqMp subst eqMp subst eqMp 624 remove 169 ref 6 ref 140 ref 171 ref appTerm 161 ref appTerm appTerm 161 remove appTerm absTerm 753 def 171 ref appTerm 754 def betaConv nil 556 ref 753 ref appTerm 755 def axiom nil 138 ref 755 remove nil cons cons 139 ref 754 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 568 ref 561 ref 753 remove nil cons cons 607 ref 171 remove nil cons cons nil cons cons nil cons cons 215 ref subst eqMp eqMp subst trans sym 172 ref eqMp 756 def subst eqMp eqMp nil 138 ref 41 ref 509 ref appTerm nil cons cons 139 ref 510 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 374 ref 201 ref 509 remove nil cons cons 450 ref cons nil cons cons 215 ref subst eqMp eqMp nil 138 ref 508 remove nil cons cons 139 ref 507 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 366 ref 367 ref 506 remove nil cons cons 370 ref cons nil cons cons 215 ref subst eqMp eqMp sym subst subst 757 def appThm eqMp 493 remove 494 remove 322 ref 316 ref 62 remove 1 ref 1 ref 1 ref 497 remove 11 ref cons opType 758 def 3 ref cons opType 759 def 758 ref nil cons 760 def cons opType constTerm "fn" 758 remove var 761 def 41 ref 432 ref 69 ref 322 ref 316 ref 761 ref varTerm 502 ref appTerm appTerm 762 def 323 ref appTerm absTerm appTerm absTerm appTerm absTerm 763 def appTerm 764 def 502 remove appTerm appTerm 323 ref appTerm absTerm 765 def 323 ref appTerm 766 def betaConv 432 ref 69 ref 765 ref appTerm 767 def absTerm 768 def 435 ref appTerm 769 def betaConv 763 ref 764 remove appTerm 770 def betaConv 91 ref 1 ref 759 ref 3 ref cons opType constTerm 771 def refl 761 remove 513 remove 432 ref 514 remove 322 ref 762 remove refl 432 remove 322 ref 323 ref absTerm 772 def absTerm 773 def 435 remove appTerm betaConv 517 remove appThm 772 remove 323 ref appTerm betaConv trans appThm absThm appThm absThm appThm absThm appThm "C" 11 ref cons nil cons "_1343" 1 ref 9 ref 1 ref 10 ref 11 remove cons opType nil cons cons opType var 773 remove nil cons cons nil cons nil cons cons 609 remove subst eqMp nil 138 ref 771 remove 763 ref appTerm nil cons cons 139 ref 770 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp "A" 760 remove cons nil cons "p" 759 remove var 763 remove nil cons cons nil cons nil cons cons 756 ref subst eqMp eqMp nil 138 ref 41 ref 768 ref appTerm nil cons cons 139 ref 769 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 374 ref 201 ref 768 remove nil cons cons 450 remove cons nil cons cons 215 ref subst eqMp eqMp nil 138 ref 767 remove nil cons cons 139 ref 766 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 366 ref 367 ref 765 remove nil cons cons 370 ref cons nil cons cons 215 ref subst eqMp eqMp sym subst subst 774 def appThm eqMp sym trans eqMp absThm eqMp eqMp absThm eqMp eqMp "A" 64 remove cons nil cons 775 def "P" 63 ref var 776 def 453 ref nil cons 777 def cons "x" 57 ref var 778 def 474 remove nil cons cons nil cons cons nil cons cons 582 ref subst proveHyp nil 138 ref 91 ref 1 ref 63 ref 3 ref cons opType constTerm 779 def 453 remove appTerm nil cons cons 139 ref 460 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp nil "p" 63 remove var 780 def 777 remove cons nil cons nil cons cons 775 ref 88 ref cons 756 remove subst 781 def subst eqMp eqMp nil 138 ref 69 ref 458 ref appTerm nil cons cons 139 ref 459 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 366 ref 367 ref 458 remove nil cons cons 368 ref 492 remove cons nil cons 782 def cons nil cons cons 215 ref subst eqMp eqMp nil 138 ref 457 remove nil cons cons 139 ref 456 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 259 ref 258 ref 455 remove nil cons cons 282 ref 491 ref cons nil cons 783 def cons nil cons cons 215 ref subst eqMp eqMp trans trans appThm 239 remove refl 784 def 427 remove appThm nil 428 remove 66 ref 238 remove nil cons cons 429 remove cons 785 def cons nil cons cons 451 remove subst 71 ref 22 ref 65 ref "_31790" 57 remove var 786 def 69 ref 70 ref 45 ref 71 ref 22 ref 786 remove varTerm 76 ref appTerm appTerm 237 ref appTerm absTerm appTerm absTerm appTerm absTerm 787 def appTerm 788 def 76 ref appTerm appTerm 237 ref appTerm absTerm 789 def 75 ref appTerm 790 def betaConv 70 ref 45 ref 789 ref appTerm 791 def absTerm 792 def 74 ref appTerm 793 def betaConv 787 ref 788 remove appTerm 794 def betaConv 787 ref "_31788" 56 remove var 795 def 78 ref 469 remove 795 remove varTerm 796 def appTerm appTerm 229 ref 473 remove 796 remove appTerm appTerm appTerm absTerm 797 def appTerm betaConv sym nil 367 ref 70 ref 45 ref 71 ref 22 ref 797 ref 76 remove appTerm 798 def appTerm 237 remove appTerm 799 def absTerm 800 def appTerm 801 def absTerm nil cons cons nil cons nil cons cons 415 remove subst 70 ref nil 169 ref 801 remove nil cons cons nil cons nil cons cons 173 ref subst nil 258 ref 800 remove nil cons cons nil cons nil cons cons 260 ref subst 71 ref nil 169 ref 799 remove nil cons cons nil cons nil cons cons 173 ref subst 798 remove betaConv 22 ref "_31785" 24 remove var 802 def 79 ref 229 ref 802 ref varTerm appTerm 803 def appTerm absTerm 75 ref appTerm 804 def appTerm refl 802 ref 483 ref 803 ref appTerm absTerm 805 def 485 ref appTerm betaConv appThm 299 ref 804 remove betaConv appThm 483 remove 229 remove 485 remove appTerm appTerm refl appThm trans 486 remove "_31784" 10 remove var 806 def 802 remove 78 remove 806 remove varTerm appTerm 803 remove appTerm absTerm absTerm 807 def 74 remove appTerm 808 def appTerm refl 807 ref 482 remove appTerm betaConv appThm 490 remove 808 remove betaConv appThm 805 remove refl appThm trans 807 remove refl 757 remove appThm eqMp 774 remove appThm eqMp sym trans eqMp absThm eqMp eqMp absThm eqMp eqMp 775 remove 776 remove 787 ref nil cons 809 def cons 778 remove 797 remove nil cons cons nil cons cons nil cons cons 582 ref subst proveHyp nil 138 ref 779 remove 787 remove appTerm nil cons cons 139 ref 794 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp nil 780 remove 809 remove cons nil cons nil cons cons 781 remove subst eqMp eqMp nil 138 ref 69 ref 792 ref appTerm nil cons cons 139 ref 793 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 366 ref 367 ref 792 remove nil cons cons 782 remove cons nil cons cons 215 ref subst eqMp eqMp nil 138 ref 791 remove nil cons cons 139 ref 790 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 259 ref 258 ref 789 remove nil cons cons 783 ref cons nil cons cons 215 ref subst eqMp eqMp trans trans appThm sym 79 ref refl 226 remove refl 301 remove appThm nil 71 ref 302 remove cons "y" 9 remove var 810 def 375 remove cons 46 ref 491 remove cons nil cons cons cons nil cons cons 71 ref 6 ref 225 remove 52 ref appTerm 49 remove 810 ref varTerm 811 def appTerm 75 ref appTerm appTerm appTerm 388 remove 52 ref appTerm 75 ref appTerm appTerm absTerm 812 def 75 ref appTerm 813 def betaConv 810 remove 45 ref 812 ref appTerm 814 def absTerm 815 def 811 ref appTerm 816 def betaConv 46 ref 41 ref 815 ref appTerm 817 def absTerm 818 def 52 ref appTerm 819 def betaConv nil 45 ref 818 ref appTerm 820 def axiom nil 138 ref 820 remove nil cons cons 139 ref 819 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 259 ref 258 ref 818 remove nil cons cons 283 ref cons nil cons cons 215 ref subst eqMp eqMp nil 138 ref 817 remove nil cons cons 139 ref 816 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 374 ref 201 ref 815 remove nil cons cons 42 ref 811 remove nil cons cons nil cons cons nil cons cons 215 ref subst eqMp eqMp nil 138 ref 814 remove nil cons cons 139 ref 813 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 259 ref 258 ref 812 remove nil cons cons 783 ref cons nil cons cons 215 ref subst eqMp eqMp subst nil 169 ref 424 remove cons nil cons nil cons cons 173 ref subst 402 remove assume eqMp trans trans sym 172 ref eqMp nil 138 ref 227 remove nil cons cons 139 ref 231 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 232 ref 75 ref appTerm 821 def betaConv nil 262 remove 139 ref 821 remove nil cons cons nil cons cons nil cons cons 200 ref subst 259 ref 258 ref 232 remove nil cons cons 783 remove cons nil cons cons 215 ref subst eqMp eqMp eqMp appThm eqMp proveHyp proveHyp eqMp nil 178 ref 422 remove cons 179 ref 410 ref cons nil cons 822 def cons nil cons cons 192 ref subst deductAntisym eqMp eqMp eqMp nil 178 ref 420 remove cons 822 ref cons nil cons cons 192 ref subst deductAntisym eqMp eqMp absThm eqMp nil 138 ref 45 ref 282 ref 140 ref 404 ref 282 ref varTerm 823 def appTerm appTerm 409 ref appTerm absTerm appTerm nil cons cons 139 ref 140 ref 405 remove appTerm 409 ref appTerm nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 259 ref 258 ref 404 remove nil cons cons 822 ref cons nil cons cons 608 ref subst eqMp eqMp eqMp nil 178 ref 416 remove cons 822 ref cons nil cons cons 192 ref subst deductAntisym eqMp eqMp absThm eqMp nil 138 ref 69 ref 368 ref 140 ref 406 ref 368 remove varTerm appTerm appTerm 409 ref appTerm absTerm appTerm nil cons cons 139 ref 140 ref 407 ref appTerm 409 remove appTerm nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 366 ref 367 ref 406 remove nil cons cons 822 ref cons nil cons cons 608 ref subst eqMp nil 138 ref 400 ref nil cons 824 def cons 411 remove cons nil cons cons 825 def 156 ref subst 825 remove 208 ref subst 299 ref 426 remove 400 remove assume 826 def appThm nil 430 remove nil cons cons 431 remove 132 remove 316 ref 434 remove 384 remove 433 remove constTerm appTerm appTerm 323 ref appTerm absTerm 827 def 133 remove appTerm 828 def betaConv 322 remove 441 remove 827 ref appTerm 829 def absTerm 830 def 323 ref appTerm 831 def betaConv nil 69 ref 830 ref appTerm 832 def axiom nil 138 ref 832 remove nil cons cons 139 ref 831 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 366 ref 367 ref 830 remove nil cons cons 370 ref cons nil cons cons 215 ref subst eqMp eqMp nil 138 ref 829 remove nil cons cons 139 ref 828 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 446 remove 447 remove 827 remove nil cons cons 449 remove cons nil cons cons 215 ref subst eqMp eqMp subst 833 def subst trans appThm 784 remove 826 remove appThm nil 785 remove nil cons cons 833 remove subst trans appThm nil "x" 21 remove var 834 def 310 remove cons nil cons nil cons cons "A" 25 remove cons nil cons 88 remove cons nil 169 ref 496 remove 50 ref appTerm 50 ref appTerm nil cons cons nil cons nil cons cons 173 ref subst 214 remove eqMp subst 835 def subst 836 def trans sym 172 ref eqMp eqMp nil 178 ref 824 remove cons 837 def 822 ref cons nil cons cons 192 ref subst deductAntisym eqMp nil 837 remove 179 ref 407 remove nil cons cons "R" 2 ref var 838 def 410 remove cons nil cons cons cons nil cons cons nil 138 ref 140 ref 183 ref appTerm 839 def 838 ref varTerm 840 def appTerm 841 def nil cons cons 139 ref 840 ref nil cons 842 def cons nil cons cons nil cons cons 200 ref subst nil 138 ref 140 ref 181 ref appTerm 843 def 840 ref appTerm nil cons cons 139 ref 140 ref 841 remove appTerm 840 ref appTerm nil cons cons nil cons cons nil cons cons 200 ref subst "r" 2 remove var 844 def 140 ref 843 remove 844 ref varTerm 845 def appTerm appTerm 846 def 140 ref 839 remove 845 ref appTerm appTerm 845 ref appTerm appTerm absTerm 847 def 840 remove appTerm 848 def betaConv 6 ref 266 ref 181 ref appTerm 849 def 183 ref appTerm 850 def appTerm refl 139 ref 556 ref 844 ref 846 remove 140 ref 634 remove 845 ref appTerm appTerm 845 ref appTerm 851 def appTerm absTerm appTerm absTerm 183 remove appTerm betaConv appThm 165 remove 849 remove appTerm refl 138 ref 139 ref 556 ref 844 remove 140 ref 142 remove 845 remove appTerm appTerm 851 remove appTerm absTerm appTerm absTerm absTerm 852 def 181 remove appTerm betaConv appThm nil 153 remove 266 remove appTerm 852 remove appTerm axiom 190 remove appThm eqMp 186 remove appThm eqMp 850 remove assume eqMp nil 138 ref 556 remove 847 ref appTerm nil cons cons 139 ref 848 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 568 remove 561 remove 847 remove nil cons cons 607 remove 842 remove cons nil cons cons nil cons cons 215 ref subst eqMp eqMp eqMp eqMp 853 def subst proveHyp proveHyp eqMp nil 178 ref 408 remove cons 822 remove cons nil cons cons 192 ref subst deductAntisym eqMp eqMp eqMp eqMp nil 178 ref 297 remove cons 179 ref 263 ref cons nil cons 854 def cons nil cons cons 192 ref subst deductAntisym eqMp eqMp eqMp nil 178 ref 295 remove cons 854 ref cons nil cons cons 192 ref subst deductAntisym eqMp eqMp absThm eqMp nil 138 ref 45 ref 282 remove 140 ref 273 ref 823 remove appTerm appTerm 249 ref appTerm absTerm appTerm nil cons cons 139 ref 140 ref 274 remove appTerm 249 ref appTerm nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 259 ref 258 ref 273 remove nil cons cons 854 ref cons nil cons cons 608 ref subst eqMp eqMp eqMp nil 178 ref 291 remove cons 854 ref cons nil cons cons 192 ref subst deductAntisym eqMp eqMp absThm eqMp nil 138 ref 41 ref 290 remove appTerm nil cons cons 139 ref 140 ref 276 ref appTerm 249 remove appTerm nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 374 remove 201 ref 275 remove nil cons cons 854 ref cons nil cons cons 608 ref subst eqMp nil 138 ref 270 ref nil cons 855 def cons 264 ref cons nil cons cons 856 def 156 ref subst 856 remove 208 ref subst 299 ref 300 ref 270 remove assume 857 def appThm nil 312 remove nil cons cons 858 def 315 ref 349 ref 325 ref appTerm 859 def betaConv 351 ref 323 ref appTerm 860 def betaConv 353 ref 321 ref appTerm 861 def betaConv 361 remove 364 remove 192 ref subst proveHyp nil 138 ref 362 remove cons 139 ref 861 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 366 ref 367 ref 353 remove nil cons cons 369 ref cons nil cons cons 215 ref subst eqMp eqMp nil 138 ref 352 remove nil cons cons 139 ref 860 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 366 ref 367 ref 351 remove nil cons cons 370 ref cons nil cons cons 215 ref subst eqMp eqMp nil 138 ref 350 remove nil cons cons 139 ref 859 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 371 ref 372 ref 349 remove nil cons cons 373 ref cons nil cons cons 215 ref subst eqMp eqMp subst 862 def subst 863 def trans appThm 380 ref 857 remove appThm nil 381 remove nil cons cons 864 def 862 remove subst trans appThm nil 834 remove 309 remove cons nil cons nil cons cons 835 remove subst trans sym 172 ref eqMp eqMp nil 178 ref 855 remove cons 865 def 854 ref cons nil cons cons 192 ref subst deductAntisym eqMp nil 865 remove 179 ref 276 remove nil cons cons 838 remove 263 remove cons nil cons 866 def cons cons nil cons cons 853 ref subst proveHyp proveHyp eqMp nil 178 ref 286 ref cons 854 ref cons nil cons cons 192 ref subst deductAntisym eqMp nil 138 ref 269 ref nil cons 867 def cons 264 remove cons nil cons cons 868 def 156 ref subst 868 remove 208 ref subst 299 ref 300 ref 269 remove assume 869 def appThm 858 ref 315 ref 343 ref 325 remove appTerm 870 def betaConv 345 ref 323 remove appTerm 871 def betaConv 347 ref 321 remove appTerm 872 def betaConv 357 remove 359 remove 192 ref subst proveHyp nil 138 ref 358 remove cons 139 ref 872 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 366 ref 367 ref 347 remove nil cons cons 369 remove cons nil cons cons 215 ref subst eqMp eqMp nil 138 ref 346 remove nil cons cons 139 ref 871 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 366 remove 367 remove 345 remove nil cons cons 370 remove cons nil cons cons 215 ref subst eqMp eqMp nil 138 ref 344 remove nil cons cons 139 ref 870 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 371 remove 372 remove 343 remove nil cons cons 373 remove cons nil cons cons 215 ref subst eqMp eqMp subst 873 def subst 874 def trans appThm 380 remove 869 remove appThm 864 remove 873 remove subst trans appThm 836 remove trans sym 172 remove eqMp eqMp nil 178 ref 867 remove cons 875 def 854 ref cons nil cons cons 192 ref subst deductAntisym eqMp nil 875 remove 179 ref 286 remove cons 866 remove cons cons nil cons cons 853 remove subst proveHyp proveHyp eqMp nil 178 ref 284 remove cons 854 ref cons nil cons cons 192 ref subst deductAntisym eqMp eqMp eqMp nil 178 ref 261 remove cons 854 remove cons nil cons cons 192 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp nil 138 ref 222 ref 255 remove appTerm nil cons cons 139 ref 101 remove 102 ref 45 ref 46 ref 22 ref 103 ref 52 ref appTerm appTerm 247 remove appTerm absTerm 876 def appTerm 877 def absTerm 878 def appTerm 879 def nil cons 880 def cons nil cons cons nil cons cons 200 ref subst proveHyp nil "h" 1 ref 26 ref 27 remove cons opType var 245 remove nil cons cons nil cons nil cons cons 315 remove "h" 1 ref 317 ref 318 remove cons opType 881 def var 882 def 140 ref 8 ref 1 ref 1 ref 317 ref 3 ref cons opType 3 ref cons opType 883 def constTerm 884 def "f" 317 ref var 885 def 884 remove "g" 317 ref var 886 def 45 ref 46 ref 140 ref 45 ref 71 ref 228 remove 316 ref 885 remove varTerm 887 def 75 ref appTerm appTerm 886 remove varTerm 888 def 75 ref appTerm appTerm appTerm absTerm appTerm appTerm 316 ref 882 remove varTerm 889 def 887 remove appTerm 52 ref appTerm appTerm 889 ref 888 remove appTerm 52 ref appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm appTerm 91 remove 883 remove constTerm "fn" 317 remove var 890 def 45 ref 46 ref 316 remove 890 remove varTerm 891 def 52 ref appTerm appTerm 889 ref 891 remove appTerm 52 ref appTerm appTerm absTerm appTerm absTerm appTerm appTerm absTerm 892 def 889 ref appTerm 893 def betaConv nil 8 remove 1 ref 1 remove 881 ref 3 ref cons opType 894 def 3 remove cons opType constTerm 892 ref appTerm 895 def axiom nil 138 ref 895 remove nil cons cons 139 ref 893 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp "A" 881 ref nil cons cons nil cons "P" 894 remove var 892 remove nil cons cons "x" 881 remove var 889 remove nil cons cons nil cons cons nil cons cons 215 ref subst eqMp eqMp subst subst eqMp nil 138 ref 880 remove cons 139 ref 220 ref cons nil cons 896 def cons nil cons cons 200 ref subst nil 221 ref 102 ref 140 ref 878 ref 103 ref appTerm 897 def appTerm 217 ref appTerm 898 def absTerm nil cons cons nil cons nil cons cons 257 remove subst 102 remove nil 169 ref 898 remove nil cons cons nil cons nil cons cons 173 ref subst nil 138 ref 897 ref nil cons 899 def cons 896 ref cons nil cons cons 900 def 156 ref subst 900 remove 208 ref subst 897 ref betaConv 897 remove assume eqMp nil 138 ref 877 remove nil cons 901 def cons 902 def 896 remove cons nil cons cons 903 def 200 ref subst proveHyp 903 ref 156 remove subst 903 remove 208 ref subst 120 remove sym 299 ref nil 46 ref 34 ref nil cons cons nil cons nil cons cons 876 ref 52 ref appTerm 904 def betaConv nil 902 remove 139 ref 904 remove nil cons cons nil cons cons nil cons cons 200 ref subst 259 remove 258 ref 876 remove nil cons cons 283 remove cons nil cons cons 215 ref subst eqMp eqMp 905 def subst appThm 35 ref refl appThm sym 300 ref 34 ref refl appThm 874 remove trans eqMp nil 138 ref 104 remove nil cons cons 139 ref 116 remove nil cons cons nil cons cons nil cons cons 208 ref subst proveHyp 299 ref nil 46 ref 37 ref nil cons cons nil cons nil cons cons 905 ref subst appThm 38 ref refl appThm sym 300 ref 37 ref refl appThm 863 remove trans eqMp nil 138 ref 105 remove nil cons cons 139 ref 115 remove nil cons cons nil cons cons nil cons cons 208 remove subst proveHyp nil 201 remove 114 remove nil cons cons nil cons nil cons cons 219 remove subst 42 ref nil 169 ref 113 remove nil cons cons nil cons nil cons cons 173 ref subst nil 258 remove 112 remove nil cons cons nil cons nil cons cons 260 remove subst 46 ref nil 169 remove 111 remove nil cons cons nil cons nil cons cons 173 remove subst 299 remove nil 46 ref 53 ref nil cons cons nil cons nil cons cons 905 remove subst appThm 110 remove refl appThm sym 300 remove 53 ref refl appThm 858 remove 377 remove subst 378 remove 52 ref refl appThm 306 remove 52 remove appTerm betaConv trans trans trans eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp eqMp eqMp 256 ref 221 ref 117 remove nil cons cons "x" 26 remove var 906 def 103 remove nil cons cons nil cons cons nil cons cons 582 remove subst proveHyp eqMp nil 178 ref 901 remove cons 179 ref 220 remove cons nil cons 907 def cons nil cons cons 192 ref subst deductAntisym eqMp eqMp eqMp nil 178 ref 899 remove cons 907 ref cons nil cons cons 192 ref subst deductAntisym eqMp eqMp absThm eqMp nil 138 ref 222 remove 906 ref 140 ref 878 ref 906 remove varTerm appTerm appTerm 217 ref appTerm absTerm appTerm nil cons cons 139 ref 140 remove 879 remove appTerm 217 remove appTerm nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 256 remove 221 remove 878 remove nil cons cons 907 remove cons nil cons cons 608 remove subst eqMp eqMp proveHyp eqMp absThm eqMp eqMp eqMp eqMp defineConstList 908 def pop hdTl pop 28 remove constTerm 31 ref appTerm 909 def 34 remove appTerm appTerm 35 remove appTerm absTerm 910 def 31 ref appTerm betaConv 911 def appThm 17 ref 18 ref 22 ref 909 ref 37 remove appTerm appTerm 38 remove appTerm 912 def appTerm 41 ref 42 ref 45 ref 46 remove 22 remove 909 ref 53 remove appTerm appTerm 61 remove 65 remove 66 remove 69 remove 70 remove 45 remove 71 remove 77 remove 79 remove 909 remove 75 remove appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm appTerm 82 remove appTerm appTerm absTerm appTerm absTerm appTerm 913 def appTerm absTerm 914 def 31 ref appTerm betaConv 915 def appThm absThm appThm appThm 19 ref 16 ref 17 ref 911 remove absThm appThm appThm 16 ref 17 ref 915 remove absThm appThm appThm appThm nil "p" 14 ref var 916 def 910 ref nil cons cons "q" 14 remove var 917 def 914 remove nil cons cons nil cons cons nil cons cons 218 remove "q" 39 remove var 918 def 6 remove 41 ref 42 ref 18 ref 557 remove appTerm 918 remove varTerm 919 def 50 remove appTerm 920 def appTerm absTerm appTerm appTerm 18 ref 41 ref 625 remove appTerm appTerm 41 remove 42 remove 920 remove absTerm appTerm appTerm appTerm absTerm 921 def 919 ref appTerm 922 def betaConv 94 remove 665 ref 921 ref appTerm 923 def absTerm 924 def 95 remove appTerm 925 def betaConv nil 665 remove 924 ref appTerm 926 def axiom nil 138 ref 926 remove nil cons cons 139 ref 925 remove nil cons cons nil cons cons nil cons cons 200 ref subst proveHyp 667 ref 668 ref 924 remove nil cons cons 670 remove cons nil cons cons 215 ref subst eqMp eqMp nil 138 remove 923 remove nil cons cons 139 remove 922 remove nil cons cons nil cons cons nil cons cons 200 remove subst proveHyp 667 remove 668 remove 921 remove nil cons cons 669 remove 919 remove nil cons cons nil cons cons nil cons cons 215 remove subst eqMp eqMp subst 927 def subst eqMp 18 ref 15 ref 910 remove appTerm 928 def appTerm refl 7 remove 16 ref 17 ref 19 ref 17 ref 912 remove absTerm 929 def 31 ref appTerm betaConv 930 def appThm 17 ref 913 remove absTerm 931 def 31 remove appTerm betaConv 932 def appThm absThm appThm appThm 19 remove 16 ref 17 ref 930 remove absThm appThm appThm 16 remove 17 remove 932 remove absThm appThm appThm appThm nil 916 remove 929 ref nil cons cons 917 remove 931 ref nil cons cons nil cons cons nil cons cons 927 remove subst eqMp appThm trans 908 remove eqMp 933 def nil 178 ref 928 ref nil cons cons 179 ref 18 remove 15 ref 929 remove appTerm 934 def appTerm 15 remove 931 remove appTerm 935 def appTerm nil cons cons nil cons cons nil cons cons 936 def 360 ref subst proveHyp 937 def nil 178 remove 934 ref nil cons cons 179 remove 935 ref nil cons cons nil cons cons nil cons cons 938 def 192 ref subst proveHyp nil 934 remove thm 933 remove 936 remove 192 remove subst proveHyp nil 928 remove thm 937 remove 938 remove 360 remove subst proveHyp nil 935 remove thm