path: "vendor/opentheory/data/theories/pair-thm/pair-thm.art"
6 version nil "P" "->" typeOp 0 def "Data.Pair.*" typeOp 1 def "A" varType 2 def "B" varType 3 def nil cons 4 def cons 5 def opType 6 def "bool" typeOp nil opType 7 def nil cons 8 def cons opType 9 def var 10 def "x" 6 ref var 11 def "=" const 12 def 0 ref 6 ref 9 ref nil cons 13 def cons opType constTerm 14 def "Data.Pair.," const 15 def 0 ref 2 ref 0 ref 3 ref 6 ref nil cons 16 def cons opType nil cons cons opType constTerm 17 def "Data.Pair.fst" const 18 def 0 ref 6 ref 2 ref nil cons 19 def cons opType 20 def constTerm 21 def 11 ref varTerm 22 def appTerm 23 def appTerm "Data.Pair.snd" const 24 def 0 ref 6 ref 4 ref cons opType 25 def constTerm 26 def 22 ref appTerm 27 def appTerm 28 def appTerm 29 def 22 ref appTerm 30 def absTerm 31 def nil cons cons 32 def nil cons nil cons cons "A" 16 ref cons 33 def nil cons 34 def nil nil cons 35 def cons 36 def 12 ref 0 ref 7 ref 0 ref 7 ref 8 ref cons opType 37 def nil cons cons opType 38 def constTerm 39 def "Data.Bool.!" const 40 def 0 ref 0 ref 2 ref 8 ref cons opType 41 def 8 ref cons opType 42 def constTerm 43 def "P" 41 ref var 44 def varTerm 45 def appTerm 46 def appTerm refl "p" 41 ref var 47 def 12 ref 0 ref 41 ref 42 ref nil cons cons opType constTerm 47 ref varTerm 48 def appTerm "x" 2 ref var 49 def "Data.Bool.T" const 7 ref constTerm 50 def absTerm 51 def appTerm absTerm 52 def 45 ref appTerm betaConv 53 def appThm nil 12 ref 0 ref 42 ref 0 ref 42 ref 8 ref cons opType 54 def nil cons cons opType constTerm 55 def 43 ref appTerm 52 remove appTerm axiom 56 def 45 ref refl 57 def appThm 58 def eqMp sym 59 def subst 60 def subst 11 ref nil "t" 7 ref var 61 def 30 ref nil cons 62 def cons nil cons nil cons cons 39 ref 61 ref varTerm 63 def appTerm 64 def 50 ref appTerm 65 def assume sym nil 50 ref axiom 66 def eqMp 63 ref assume 66 ref deductAntisym deductAntisym 67 def subst 11 ref "Data.Bool.?" const 68 def 42 ref constTerm 69 def "a" 2 ref var 70 def 68 ref 0 ref 0 ref 3 ref 8 ref cons opType 71 def 8 ref cons opType 72 def constTerm 73 def "b" 3 ref var 74 def 14 ref 22 ref appTerm 75 def 17 ref 70 ref varTerm 76 def appTerm 77 def 74 ref varTerm 78 def appTerm 79 def appTerm 80 def absTerm 81 def appTerm 82 def absTerm 83 def appTerm 84 def absTerm 85 def 22 ref appTerm 86 def betaConv nil 40 ref 0 ref 9 ref 8 ref cons opType 87 def constTerm 88 def 85 ref appTerm 89 def axiom nil "p" 7 ref var 90 def 89 remove nil cons cons "q" 7 ref var 91 def 86 remove nil cons cons nil cons cons nil cons cons 39 ref "Data.Bool.==>" const 38 ref constTerm 92 def 90 ref varTerm 93 def appTerm 94 def 91 ref varTerm 95 def appTerm 96 def appTerm 97 def refl 90 ref 91 ref 39 ref "Data.Bool./\\" const 38 ref constTerm 98 def 93 ref appTerm 99 def 95 ref appTerm 100 def appTerm 101 def 93 ref appTerm absTerm 102 def absTerm 103 def 93 ref appTerm betaConv 95 ref refl 104 def appThm 102 remove 95 ref appTerm betaConv trans appThm nil 12 ref 0 ref 38 ref 0 ref 38 ref 8 ref cons opType 105 def nil cons cons opType constTerm 106 def 92 ref appTerm 103 remove appTerm axiom 93 ref refl 107 def appThm 104 ref appThm eqMp 108 def sym 109 def 101 remove refl 91 ref 12 ref 0 ref 105 ref 0 ref 105 remove 8 ref cons opType nil cons cons opType constTerm 110 def "f" 38 ref var 111 def 111 ref varTerm 112 def 93 ref appTerm 95 ref appTerm absTerm 113 def appTerm 111 ref 112 ref 50 ref appTerm 50 ref appTerm absTerm 114 def appTerm absTerm 115 def 95 ref appTerm betaConv appThm 12 ref 0 ref 37 ref 0 ref 37 ref 8 ref cons opType 116 def nil cons cons opType constTerm 117 def 99 ref appTerm refl 90 ref 115 remove absTerm 118 def 93 ref appTerm betaConv appThm nil 106 ref 98 ref appTerm 118 ref appTerm axiom 119 def 107 remove appThm eqMp 104 ref appThm eqMp 120 def sym 111 ref 112 ref refl nil 61 ref 93 ref nil cons 121 def cons nil cons nil cons cons 122 def 67 ref subst 93 ref assume 123 def eqMp appThm nil 61 ref 95 ref nil cons 124 def cons nil cons nil cons cons 125 def 67 ref subst 95 ref assume 126 def eqMp appThm absThm eqMp 127 def nil "P" 7 ref var 128 def 121 ref cons 129 def "Q" 7 ref var 130 def 124 ref cons nil cons 131 def cons nil cons cons 39 ref refl 132 def 111 ref 112 remove 128 ref varTerm 133 def appTerm 134 def 130 ref varTerm 135 def appTerm absTerm 136 def 90 ref 91 ref 93 ref absTerm absTerm 137 def appTerm betaConv 137 ref 133 ref appTerm betaConv 135 ref refl 138 def appThm 91 ref 133 ref absTerm 135 ref appTerm betaConv trans trans appThm 114 ref 137 ref appTerm betaConv 137 ref 50 ref appTerm betaConv 50 ref refl 139 def appThm 91 ref 50 ref absTerm 50 ref appTerm betaConv trans trans appThm 39 ref 98 ref 133 ref appTerm 140 def 135 ref appTerm 141 def appTerm refl 91 ref 110 remove 111 remove 134 remove 95 ref appTerm absTerm appTerm 114 ref appTerm absTerm 135 ref appTerm betaConv appThm 117 ref 140 remove appTerm refl 118 remove 133 ref appTerm betaConv appThm 119 remove 133 ref refl 142 def appThm eqMp 138 ref appThm eqMp 141 remove assume eqMp 143 def 137 remove refl appThm eqMp sym 66 ref eqMp 144 def subst 145 def deductAntisym eqMp 108 remove 96 ref assume eqMp sym 123 ref eqMp 132 ref 113 remove 90 ref 91 ref 95 ref absTerm 146 def absTerm 147 def appTerm betaConv 147 ref 93 ref appTerm betaConv 104 ref appThm 146 ref 95 ref appTerm betaConv trans trans appThm 114 remove 147 ref appTerm betaConv 147 ref 50 ref appTerm betaConv 139 ref appThm 146 ref 50 ref appTerm betaConv trans trans 148 def appThm 120 remove 100 remove assume eqMp 147 ref refl 149 def appThm eqMp sym 66 ref eqMp 150 def proveHyp 151 def deductAntisym 152 def subst proveHyp 34 ref 10 ref 85 remove nil cons cons 11 ref 22 ref nil cons 153 def cons nil cons 154 def cons nil cons cons nil 90 ref 46 ref nil cons 155 def cons 91 ref 45 ref 49 ref varTerm 156 def appTerm 157 def nil cons 158 def cons nil cons cons nil cons cons 159 def 109 ref subst 159 remove 150 remove 127 remove deductAntisym 160 def subst 39 ref 157 ref appTerm refl 51 remove 156 ref appTerm betaConv appThm 53 remove 58 remove 46 remove assume eqMp eqMp 156 ref refl 161 def appThm eqMp sym 66 ref eqMp eqMp nil 128 ref 155 remove cons 130 ref 158 ref cons nil cons cons nil cons cons 144 ref subst deductAntisym eqMp 162 def subst eqMp eqMp nil 90 ref 84 ref nil cons cons 91 ref 62 ref cons nil cons 163 def cons nil cons cons 152 ref subst proveHyp nil 44 ref 70 ref 92 ref 83 ref 76 ref appTerm 164 def appTerm 30 ref appTerm 165 def absTerm nil cons cons nil cons nil cons cons 59 ref subst 70 ref nil 61 ref 165 remove nil cons cons nil cons nil cons cons 67 ref subst nil 90 ref 164 ref nil cons 166 def cons 163 ref cons nil cons cons 167 def 109 ref subst 167 remove 160 ref subst 164 ref betaConv 164 remove assume eqMp nil 90 ref 82 ref nil cons cons 163 ref cons nil cons cons 152 ref subst proveHyp nil "P" 71 ref var 168 def 74 ref 92 ref 81 ref 78 ref appTerm 169 def appTerm 30 ref appTerm 170 def absTerm nil cons cons nil cons nil cons cons "A" 4 ref cons 171 def nil cons 172 def 35 ref cons 173 def 59 ref subst 174 def subst 74 ref nil 61 ref 170 remove nil cons cons nil cons nil cons cons 67 ref subst nil 90 ref 169 ref nil cons 175 def cons 163 ref cons nil cons cons 176 def 109 ref subst 176 remove 160 ref subst 169 ref betaConv 169 remove assume eqMp nil 90 ref 80 ref nil cons 177 def cons 163 remove cons nil cons cons 178 def 152 ref subst proveHyp 178 ref 109 ref subst 178 remove 160 ref subst 39 ref "_1259" 6 ref var 179 def 14 ref 17 ref 21 ref 179 remove varTerm 180 def appTerm appTerm 26 ref 180 ref appTerm appTerm appTerm 180 remove appTerm absTerm 181 def 22 ref appTerm 182 def appTerm refl 181 remove 79 ref appTerm betaConv appThm 132 ref 182 remove betaConv appThm 14 ref 17 ref 21 ref 79 ref appTerm 183 def appTerm 26 ref 79 ref appTerm 184 def appTerm appTerm 79 ref appTerm refl appThm trans 31 ref refl 80 remove assume appThm eqMp sym 17 ref refl 74 ref 12 ref 0 ref 2 ref 41 ref nil cons 185 def cons opType constTerm 186 def 183 remove appTerm 76 ref appTerm absTerm 187 def 78 ref appTerm 188 def betaConv 70 ref 40 ref 72 ref constTerm 189 def 187 ref appTerm 190 def absTerm 191 def 76 ref appTerm 192 def betaConv nil 43 ref 191 ref appTerm 193 def axiom nil 90 ref 193 remove nil cons cons 91 ref 192 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp "A" 19 ref cons 194 def nil cons 195 def 44 ref 191 remove nil cons cons 49 ref 76 ref nil cons cons nil cons 196 def cons nil cons cons 162 ref subst eqMp eqMp nil 90 ref 190 remove nil cons cons 91 ref 188 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 172 ref 168 ref 187 remove nil cons cons "x" 3 ref var 197 def 78 ref nil cons 198 def cons nil cons 199 def cons nil cons cons 162 ref subst eqMp eqMp 200 def appThm 74 ref 12 ref 0 ref 3 ref 71 ref nil cons 201 def cons opType constTerm 202 def 184 remove appTerm 78 ref appTerm absTerm 203 def 78 ref appTerm 204 def betaConv 70 ref 189 ref 203 ref appTerm 205 def absTerm 206 def 76 ref appTerm 207 def betaConv nil 43 ref 206 ref appTerm 208 def axiom nil 90 ref 208 remove nil cons cons 91 ref 207 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 195 ref 44 ref 206 remove nil cons cons 196 ref cons nil cons cons 162 ref subst eqMp eqMp nil 90 ref 205 remove nil cons cons 91 ref 204 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 172 ref 168 ref 203 remove nil cons cons 199 ref cons nil cons cons 162 ref subst eqMp eqMp 209 def appThm eqMp eqMp nil 128 ref 177 remove cons 130 ref 62 ref cons nil cons 210 def cons nil cons cons 144 ref subst deductAntisym eqMp eqMp eqMp nil 128 ref 175 remove cons 210 ref cons nil cons cons 144 ref subst deductAntisym eqMp eqMp absThm eqMp nil 90 ref 189 ref 197 ref 92 ref 81 ref 197 ref varTerm 211 def appTerm appTerm 30 ref appTerm absTerm appTerm nil cons cons 91 ref 92 ref 82 remove appTerm 30 ref appTerm nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 172 ref 168 ref 81 remove nil cons cons 210 ref cons nil cons cons nil 90 ref 43 ref 49 ref 92 ref 157 ref appTerm 212 def 135 ref appTerm 213 def absTerm 214 def appTerm 215 def nil cons 216 def cons 217 def 91 ref 92 ref 69 ref 45 ref appTerm 218 def appTerm 219 def 135 ref appTerm nil cons 220 def cons nil cons cons nil cons cons 221 def 109 ref subst 221 remove 160 ref subst nil 90 ref 218 ref nil cons 222 def cons 223 def 91 ref 135 ref nil cons 224 def cons nil cons 225 def cons nil cons cons 226 def 109 ref subst 226 remove 160 ref subst nil 217 ref 225 ref cons nil cons cons 227 def 152 ref subst 91 ref 92 ref 43 ref 49 ref 212 remove 95 ref appTerm absTerm appTerm appTerm 95 ref appTerm absTerm 228 def 135 ref appTerm 229 def betaConv nil 223 remove 91 ref 40 ref 116 remove constTerm 230 def 228 ref appTerm 231 def nil cons 232 def cons nil cons cons nil cons cons 233 def 152 ref subst 39 ref 218 remove appTerm 234 def refl 47 ref 230 ref 91 ref 92 ref 43 ref 49 ref 92 ref 48 ref 156 ref appTerm 235 def appTerm 236 def 95 ref appTerm absTerm appTerm appTerm 95 ref appTerm absTerm appTerm absTerm 237 def 45 ref appTerm betaConv appThm nil 55 remove 69 ref appTerm 237 remove appTerm axiom 57 remove appThm eqMp 238 def nil 90 ref 234 remove 231 ref appTerm nil cons cons 91 ref 219 remove 231 remove appTerm nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 233 remove nil 90 ref 39 ref 93 ref appTerm 239 def 95 ref appTerm 240 def nil cons 241 def cons 242 def 91 ref 96 ref nil cons 243 def cons nil cons 244 def cons nil cons cons 245 def 109 ref subst 245 remove 160 ref subst 109 ref 160 ref 240 ref assume 246 def 123 remove eqMp eqMp 145 ref deductAntisym eqMp 247 def eqMp nil 128 ref 241 remove cons 248 def 130 ref 243 ref cons nil cons 249 def cons nil cons cons 144 ref subst deductAntisym eqMp 250 def subst eqMp eqMp nil 90 ref 232 remove cons 91 ref 229 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp "A" 8 ref cons nil cons 251 def "P" 37 ref var 252 def 228 remove nil cons cons "x" 7 ref var 253 def 224 ref cons nil cons cons nil cons cons 162 ref subst eqMp eqMp eqMp eqMp nil 128 ref 222 remove cons 130 ref 224 remove cons nil cons 254 def cons nil cons cons 144 ref subst deductAntisym eqMp eqMp nil 128 ref 216 ref cons 255 def 130 ref 220 remove cons nil cons cons nil cons cons 144 ref subst deductAntisym eqMp 256 def subst eqMp eqMp eqMp nil 128 ref 166 remove cons 210 ref cons nil cons cons 144 ref subst deductAntisym eqMp eqMp absThm eqMp nil 90 ref 43 ref 49 ref 92 ref 83 ref 156 ref appTerm appTerm 30 ref appTerm absTerm appTerm nil cons cons 91 ref 92 ref 84 remove appTerm 30 ref appTerm nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 195 ref 44 ref 83 remove nil cons cons 210 remove cons nil cons cons 256 ref subst eqMp eqMp eqMp absThm eqMp 257 def nil 88 ref 31 ref appTerm 258 def thm nil 90 ref 40 ref 0 ref 87 ref 8 ref cons opType 259 def constTerm 260 def "p" 9 ref var 261 def 39 ref 88 ref 11 ref 261 ref varTerm 262 def 22 ref appTerm 263 def absTerm 264 def appTerm 265 def appTerm 43 ref 70 ref 189 ref 74 ref 262 ref 79 ref appTerm 266 def absTerm 267 def appTerm 268 def absTerm 269 def appTerm 270 def appTerm absTerm 271 def appTerm 272 def nil cons cons 273 def nil cons nil cons cons 239 ref refl 274 def nil 61 ref "Data.Bool.~" const 37 remove constTerm 275 def 93 ref appTerm 276 def nil cons 277 def cons nil cons nil cons cons 61 ref 39 ref 92 ref 63 ref appTerm 278 def "Data.Bool.F" const 7 ref constTerm 279 def appTerm appTerm 275 ref 63 ref appTerm 280 def appTerm absTerm 281 def 63 ref appTerm 282 def betaConv nil 230 ref 281 ref appTerm 283 def axiom nil 90 ref 283 remove nil cons cons 91 ref 282 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 251 ref 252 ref 281 remove nil cons cons 253 ref 63 ref nil cons cons nil cons 284 def cons nil cons cons 162 ref subst eqMp eqMp 285 def subst appThm sym 274 remove 122 ref 61 ref 39 ref 275 ref 280 ref appTerm appTerm 63 ref appTerm absTerm 286 def 63 ref appTerm 287 def betaConv nil 230 ref 286 ref appTerm 288 def axiom nil 90 ref 288 remove nil cons cons 91 ref 287 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 251 ref 252 ref 286 remove nil cons cons 284 ref cons nil cons cons 162 ref subst eqMp eqMp 289 def subst 290 def appThm nil 253 ref 121 ref cons nil cons 291 def nil cons cons 251 ref 35 ref cons 292 def nil 61 ref 186 ref 156 ref appTerm 293 def 156 ref appTerm nil cons cons nil cons nil cons cons 67 ref subst 161 ref eqMp 294 def subst 295 def subst trans sym 66 ref eqMp eqMp 296 def subst sym nil 90 ref 275 ref 272 ref appTerm 297 def nil cons 298 def cons 91 ref 279 ref nil cons 299 def cons nil cons 300 def cons nil cons cons 301 def 109 ref subst 301 remove 160 ref subst 257 ref nil 90 ref 258 remove nil cons 302 def cons 303 def 300 ref cons nil cons cons 304 def 152 ref subst proveHyp 305 def 304 ref 109 ref subst 306 def 304 remove 160 ref subst 307 def nil "P" 87 ref var 308 def 271 ref nil cons cons 309 def nil cons nil cons cons "A" 13 ref cons nil cons 310 def 35 ref cons 311 def 132 ref 275 ref refl 312 def 43 ref refl 313 def nil "t" 41 ref var 314 def 45 ref nil cons 315 def cons nil cons nil cons cons 194 ref "B" 8 ref cons 316 def nil cons 317 def cons 35 ref cons 318 def "t" 0 ref 5 remove opType 319 def var 320 def 12 ref 0 ref 319 ref 0 ref 319 ref 8 ref cons opType 321 def nil cons cons opType constTerm 322 def 320 ref varTerm 323 def appTerm 49 ref 323 ref 156 ref appTerm absTerm 324 def appTerm 325 def absTerm 326 def 323 ref appTerm 327 def betaConv 40 ref 0 ref 321 ref 8 ref cons opType 328 def constTerm 329 def refl 330 def 320 ref 325 remove assume sym 322 ref 324 remove appTerm 323 ref appTerm 331 def assume sym deductAntisym absThm appThm nil 329 ref 320 ref 331 remove absTerm 332 def appTerm 333 def axiom 334 def eqMp nil 90 ref 329 ref 326 ref appTerm nil cons cons 91 ref 327 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp "A" 319 ref nil cons 335 def cons nil cons 336 def "P" 321 ref var 337 def 326 remove nil cons cons "x" 319 ref var 338 def 323 ref nil cons cons nil cons 339 def cons nil cons cons 162 ref subst eqMp eqMp 340 def subst subst 341 def appThm appThm appThm 69 ref 49 ref 275 ref 157 ref appTerm absTerm 342 def appTerm refl appThm sym nil 47 ref 315 ref cons nil cons nil cons cons 343 def 47 ref 39 ref 275 ref 43 ref 49 ref 235 ref absTerm 344 def appTerm appTerm appTerm 69 ref 49 ref 275 ref 235 ref appTerm 345 def absTerm 346 def appTerm appTerm absTerm 347 def 48 ref appTerm 348 def betaConv nil 40 ref 54 remove constTerm 349 def 347 ref appTerm 350 def axiom nil 90 ref 350 remove nil cons cons 91 ref 348 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp "A" 185 remove cons nil cons 351 def "P" 42 remove var 352 def 347 remove nil cons cons "x" 41 ref var 353 def 48 ref nil cons 354 def cons nil cons 355 def cons nil cons cons 162 ref subst eqMp eqMp subst eqMp 356 def subst 357 def subst 68 ref 259 remove constTerm 358 def refl 359 def 261 ref 312 ref 271 remove 262 ref appTerm 360 def betaConv 361 def appThm nil 90 ref 265 ref nil cons 362 def cons 363 def 91 ref 270 ref nil cons 364 def cons nil cons 365 def cons nil cons cons nil 90 ref 239 ref 279 ref appTerm 366 def nil cons 367 def cons 368 def 91 ref 39 ref 275 ref 240 ref appTerm appTerm "Data.Bool.\\/" const 38 remove constTerm 369 def 99 ref 275 ref 95 ref appTerm 370 def appTerm appTerm 98 ref 276 ref appTerm 95 ref appTerm appTerm appTerm nil cons 371 def cons nil cons 372 def cons nil cons cons 373 def 109 ref subst 373 remove 160 ref subst 39 ref "_550" 7 ref var 374 def 39 ref 275 ref 39 ref 374 remove varTerm 375 def appTerm 95 ref appTerm appTerm appTerm 369 ref 98 ref 375 ref appTerm 370 ref appTerm appTerm 98 ref 275 ref 375 remove appTerm appTerm 95 ref appTerm appTerm appTerm absTerm 376 def 93 ref appTerm 377 def appTerm refl 378 def 376 ref 279 ref appTerm betaConv appThm 132 ref 377 remove betaConv appThm 379 def 39 ref 275 ref 39 ref 279 ref appTerm 380 def 95 ref appTerm 381 def appTerm appTerm 369 ref 98 ref 279 ref appTerm 382 def 370 ref appTerm appTerm 98 ref 275 ref 279 ref appTerm 383 def appTerm 384 def 95 ref appTerm appTerm appTerm refl appThm trans 376 remove refl 385 def 366 remove assume 386 def appThm eqMp sym 132 ref 312 ref 125 ref 61 ref 39 ref 380 ref 63 ref appTerm appTerm 280 ref appTerm absTerm 387 def 63 ref appTerm 388 def betaConv nil 230 ref 387 ref appTerm 389 def axiom nil 90 ref 389 remove nil cons cons 91 ref 388 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 251 ref 252 ref 387 remove nil cons cons 284 ref cons nil cons cons 162 ref subst eqMp eqMp 390 def subst 391 def appThm 125 ref 289 ref subst 392 def trans appThm 369 ref refl 393 def nil 61 ref 370 ref nil cons 394 def cons nil cons nil cons cons 395 def 61 ref 39 ref 382 remove 63 ref appTerm appTerm 279 ref appTerm absTerm 396 def 63 ref appTerm 397 def betaConv nil 230 ref 396 ref appTerm 398 def axiom nil 90 ref 398 remove nil cons cons 91 ref 397 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 251 ref 252 ref 396 remove nil cons cons 284 ref cons nil cons cons 162 ref subst eqMp eqMp 399 def subst appThm 98 ref refl 400 def nil 39 ref 383 ref appTerm 401 def 50 ref appTerm axiom 402 def appThm 403 def 104 ref appThm 125 ref 61 ref 39 ref 98 ref 50 ref appTerm 404 def 63 ref appTerm appTerm 63 ref appTerm absTerm 405 def 63 ref appTerm 406 def betaConv nil 230 ref 405 ref appTerm 407 def axiom nil 90 ref 407 remove nil cons cons 91 ref 406 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 251 ref 252 ref 405 remove nil cons cons 284 ref cons nil cons cons 162 ref subst eqMp eqMp 408 def subst trans appThm 125 ref 61 ref 39 ref 369 ref 279 ref appTerm 409 def 63 ref appTerm appTerm 63 ref appTerm absTerm 410 def 63 ref appTerm 411 def betaConv nil 230 ref 410 ref appTerm 412 def axiom nil 90 ref 412 remove nil cons cons 91 ref 411 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 251 ref 252 ref 410 remove nil cons cons 284 ref cons nil cons cons 162 ref subst eqMp eqMp 413 def subst trans appThm nil 253 ref 124 ref cons nil cons 414 def nil cons cons 295 ref subst trans sym 66 ref eqMp eqMp eqMp nil 128 ref 367 ref cons 415 def 130 ref 371 ref cons nil cons 416 def cons nil cons cons 144 ref subst deductAntisym eqMp nil 90 ref 239 ref 50 ref appTerm 417 def nil cons 418 def cons 419 def 372 remove cons nil cons cons 420 def 109 ref subst 420 remove 160 ref subst 378 remove "_548" 7 ref var 421 def 39 ref 275 ref 39 ref 421 remove varTerm 422 def appTerm 95 ref appTerm appTerm appTerm 369 ref 98 ref 422 ref appTerm 370 ref appTerm appTerm 98 ref 275 ref 422 remove appTerm appTerm 95 ref appTerm appTerm appTerm absTerm 50 ref appTerm betaConv appThm 379 remove 39 ref 275 ref 39 ref 50 ref appTerm 423 def 95 ref appTerm 424 def appTerm appTerm 369 ref 404 remove 370 ref appTerm appTerm 98 ref 275 ref 50 ref appTerm 425 def appTerm 426 def 95 ref appTerm appTerm appTerm refl appThm trans 385 remove 417 remove assume 427 def appThm eqMp sym 132 ref 312 ref 125 ref 61 ref 39 ref 423 ref 63 ref appTerm appTerm 63 ref appTerm absTerm 428 def 63 ref appTerm 429 def betaConv nil 230 ref 428 ref appTerm 430 def axiom nil 90 ref 430 remove nil cons cons 91 ref 429 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 251 ref 252 ref 428 remove nil cons cons 284 ref cons nil cons cons 162 ref subst eqMp eqMp 431 def subst 432 def appThm appThm 393 ref 395 ref 408 ref subst appThm 400 ref nil 39 ref 425 ref appTerm 433 def 279 ref appTerm axiom 434 def appThm 435 def 104 remove appThm 125 ref 399 ref subst trans appThm 395 ref 61 ref 39 ref 369 ref 63 ref appTerm 436 def 279 ref appTerm appTerm 63 ref appTerm absTerm 437 def 63 ref appTerm 438 def betaConv nil 230 ref 437 ref appTerm 439 def axiom nil 90 ref 439 remove nil cons cons 91 ref 438 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 251 ref 252 ref 437 remove nil cons cons 284 ref cons nil cons cons 162 ref subst eqMp eqMp 440 def subst trans appThm nil 253 ref 394 remove cons nil cons nil cons cons 295 ref subst trans sym 66 ref eqMp eqMp eqMp nil 128 ref 418 remove cons 441 def 416 remove cons nil cons cons 144 ref subst deductAntisym eqMp 61 ref 369 ref 65 ref appTerm 64 remove 279 ref appTerm appTerm absTerm 442 def 93 ref appTerm 443 def betaConv nil 230 ref 442 ref appTerm 444 def axiom 445 def nil 90 ref 444 remove nil cons cons 446 def 91 ref 443 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 251 ref 252 ref 442 ref nil cons cons 447 def 291 ref cons nil cons cons 162 ref subst eqMp eqMp 448 def nil 441 ref 130 ref 367 remove cons 449 def "R" 7 ref var 450 def 371 remove cons nil cons cons cons nil cons cons nil 90 ref 92 ref 135 ref appTerm 451 def 450 ref varTerm 452 def appTerm 453 def nil cons cons 91 ref 452 ref nil cons 454 def cons nil cons cons nil cons cons 152 ref subst nil 90 ref 92 ref 133 ref appTerm 455 def 452 ref appTerm nil cons cons 91 ref 92 ref 453 remove appTerm 452 ref appTerm nil cons cons nil cons cons nil cons cons 152 ref subst "r" 7 ref var 456 def 92 ref 455 ref 456 ref varTerm 457 def appTerm appTerm 458 def 92 ref 451 remove 457 ref appTerm appTerm 457 ref appTerm appTerm absTerm 459 def 452 remove appTerm 460 def betaConv 39 ref 369 ref 133 ref appTerm 461 def 135 ref appTerm 462 def appTerm refl 91 ref 230 ref 456 ref 458 remove 92 ref 92 ref 95 ref appTerm 463 def 457 ref appTerm 464 def appTerm 465 def 457 ref appTerm 466 def appTerm absTerm appTerm absTerm 135 ref appTerm betaConv appThm 117 ref 461 remove appTerm refl 90 ref 91 ref 230 ref 456 ref 92 ref 94 ref 457 ref appTerm 467 def appTerm 466 remove appTerm absTerm appTerm absTerm absTerm 468 def 133 ref appTerm betaConv appThm nil 106 remove 369 ref appTerm 468 remove appTerm axiom 142 ref appThm eqMp 138 ref appThm eqMp 462 remove assume eqMp nil 90 ref 230 ref 459 ref appTerm nil cons cons 91 ref 460 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 251 ref 252 ref 459 remove nil cons cons 253 ref 454 remove cons nil cons cons nil cons cons 162 ref subst eqMp eqMp eqMp eqMp 469 def subst proveHyp proveHyp proveHyp 470 def subst 393 ref 400 ref 88 ref refl 471 def 264 ref refl 472 def appThm appThm 473 def nil 44 ref 269 ref nil cons cons 474 def nil cons nil cons cons 356 ref subst 69 ref refl 475 def 70 ref 312 ref 269 ref 76 ref appTerm 476 def betaConv 477 def appThm nil 168 ref 267 ref nil cons 478 def cons 479 def nil cons nil cons cons 480 def 173 ref 356 ref subst subst 73 ref refl 481 def 74 ref 312 ref 267 ref 78 ref appTerm 482 def betaConv 483 def appThm absThm 484 def appThm trans trans absThm appThm trans appThm appThm 400 ref nil 10 ref 264 ref nil cons cons 485 def nil cons nil cons cons 486 def 36 ref 356 ref subst subst 68 ref 87 ref constTerm 487 def refl 488 def 11 ref 312 ref 264 ref 22 ref appTerm betaConv appThm absThm 489 def appThm trans appThm 313 ref 70 ref 189 ref refl 490 def 74 ref 266 ref refl absThm 491 def appThm absThm appThm 492 def appThm appThm trans trans absThm appThm trans 132 ref 359 ref 261 ref 393 ref 261 ref 98 ref 265 ref appTerm 493 def 69 ref 70 ref 73 ref 74 ref 275 ref 266 ref appTerm 494 def absTerm 495 def appTerm absTerm 496 def appTerm appTerm absTerm 497 def 262 ref appTerm betaConv 498 def appThm 261 ref 98 ref 487 ref 11 ref 275 ref 263 ref appTerm 499 def absTerm 500 def appTerm appTerm 270 ref appTerm absTerm 501 def 262 ref appTerm betaConv 502 def appThm absThm appThm appThm 393 ref 359 ref 261 ref 498 remove absThm appThm appThm 359 ref 261 ref 502 remove absThm appThm appThm appThm nil "p" 87 ref var 503 def 497 remove nil cons cons "q" 87 ref var 504 def 501 remove nil cons cons nil cons cons nil cons cons 311 ref "q" 41 ref var 505 def 39 ref 69 ref 49 ref 369 ref 235 ref appTerm 506 def 505 ref varTerm 507 def 156 ref appTerm 508 def appTerm absTerm appTerm 509 def appTerm 369 ref 69 ref 344 remove appTerm 510 def appTerm 511 def 69 ref 49 ref 508 ref absTerm appTerm 512 def appTerm 513 def appTerm absTerm 514 def 507 ref appTerm 515 def betaConv 47 ref 349 ref 514 ref appTerm 516 def absTerm 517 def 48 ref appTerm 518 def betaConv nil 349 ref 517 ref appTerm 519 def axiom nil 90 ref 519 remove nil cons cons 91 ref 518 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 351 ref 352 ref 517 remove nil cons cons 355 ref cons nil cons cons 162 ref subst eqMp eqMp nil 90 ref 516 remove nil cons cons 91 ref 515 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 351 ref 352 ref 514 remove nil cons cons 353 ref 507 ref nil cons cons nil cons 520 def cons nil cons cons 162 ref subst eqMp eqMp subst 521 def subst eqMp 393 ref 359 ref 261 ref 132 ref 473 ref 475 ref 70 ref 496 ref 76 ref appTerm betaConv 522 def absThm appThm appThm appThm 475 ref 70 ref 473 ref 522 remove appThm absThm appThm appThm nil 505 ref 496 remove nil cons cons 363 ref nil cons 523 def cons nil cons cons 505 ref 39 ref 99 ref 512 ref appTerm appTerm 69 ref 49 ref 99 remove 508 ref appTerm absTerm appTerm appTerm absTerm 524 def 507 ref appTerm 525 def betaConv 90 ref 349 ref 524 ref appTerm 526 def absTerm 527 def 93 ref appTerm 528 def betaConv nil 230 ref 527 ref appTerm 529 def axiom nil 90 ref 529 remove nil cons cons 91 ref 528 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 251 ref 252 ref 527 remove nil cons cons 291 ref cons nil cons cons 162 ref subst eqMp eqMp nil 90 ref 526 remove nil cons cons 91 ref 525 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 351 ref 352 ref 524 remove nil cons cons 520 ref cons nil cons cons 162 ref subst eqMp eqMp 530 def subst eqMp 475 ref 70 ref 132 ref 473 ref 481 ref 74 ref 495 ref 78 ref appTerm betaConv 531 def absThm appThm appThm appThm 481 ref 74 ref 473 remove 531 remove appThm absThm appThm appThm nil "q" 71 ref var 532 def 495 ref nil cons cons 523 remove cons nil cons cons 173 ref 530 ref subst 533 def subst eqMp absThm appThm trans absThm appThm appThm 359 ref 261 ref 132 ref 400 ref 488 ref 11 ref 500 ref 22 ref appTerm betaConv 534 def absThm appThm appThm 492 ref appThm appThm 488 ref 11 ref 400 ref 534 remove appThm 492 remove appThm absThm appThm appThm nil 261 ref 500 ref nil cons 535 def cons 365 remove cons nil cons cons 36 ref 91 ref 39 ref 98 ref 510 ref appTerm 95 ref appTerm appTerm 69 ref 49 ref 98 ref 235 ref appTerm 536 def 95 ref appTerm absTerm appTerm appTerm absTerm 537 def 95 ref appTerm 538 def betaConv 47 ref 230 ref 537 ref appTerm 539 def absTerm 540 def 48 ref appTerm 541 def betaConv nil 349 ref 540 ref appTerm 542 def axiom nil 90 ref 542 remove nil cons cons 91 ref 541 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 351 ref 352 ref 540 remove nil cons cons 355 ref cons nil cons cons 162 ref subst eqMp eqMp nil 90 ref 539 remove nil cons cons 91 ref 538 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 251 ref 252 ref 537 remove nil cons cons 414 ref cons nil cons cons 162 ref subst eqMp eqMp 543 def subst 544 def subst eqMp absThm appThm appThm 132 ref 393 ref 359 ref 261 ref 261 ref 69 ref 70 ref 73 ref 74 ref 493 remove 494 ref appTerm 545 def absTerm 546 def appTerm absTerm 547 def appTerm absTerm 548 def 262 ref appTerm betaConv 549 def absThm appThm appThm 359 ref 261 ref 261 ref 487 ref 11 ref 98 ref 499 ref appTerm 270 ref appTerm 550 def absTerm 551 def appTerm 552 def absTerm 553 def 262 ref appTerm betaConv 554 def absThm appThm appThm appThm 359 ref 261 ref 393 ref 549 remove appThm 554 remove appThm absThm appThm appThm nil 503 ref 548 remove nil cons cons 504 ref 553 remove nil cons cons nil cons cons nil cons cons 311 ref 505 ref 39 ref 513 remove appTerm 509 remove appTerm absTerm 555 def 507 ref appTerm 556 def betaConv 47 ref 349 ref 555 ref appTerm 557 def absTerm 558 def 48 ref appTerm 559 def betaConv nil 349 ref 558 ref appTerm 560 def axiom nil 90 ref 560 remove nil cons cons 91 ref 559 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 351 ref 352 ref 558 remove nil cons cons 355 ref cons nil cons cons 162 ref subst eqMp eqMp nil 90 ref 557 remove nil cons cons 91 ref 556 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 351 ref 352 ref 555 remove nil cons cons 520 ref cons nil cons cons 162 ref subst eqMp eqMp 561 def subst 562 def subst eqMp 359 ref 261 ref 132 ref 393 ref 475 ref 70 ref 547 ref 76 ref appTerm betaConv 563 def absThm appThm appThm 552 ref refl 564 def appThm appThm 475 ref 70 ref 393 ref 563 remove appThm 564 ref appThm absThm appThm appThm nil 47 ref 547 remove nil cons cons 91 ref 552 remove nil cons cons nil cons 565 def cons nil cons cons 91 ref 39 ref 511 remove 95 ref appTerm appTerm 69 ref 49 ref 506 remove 95 ref appTerm absTerm appTerm appTerm absTerm 566 def 95 ref appTerm 567 def betaConv 47 ref 230 ref 566 ref appTerm 568 def absTerm 569 def 48 ref appTerm 570 def betaConv nil 349 ref 569 ref appTerm 571 def axiom nil 90 ref 571 remove nil cons cons 91 ref 570 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 351 ref 352 ref 569 remove nil cons cons 355 ref cons nil cons cons 162 ref subst eqMp eqMp nil 90 ref 568 remove nil cons cons 91 ref 567 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 251 ref 252 ref 566 remove nil cons cons 414 remove cons nil cons cons 162 ref subst eqMp eqMp 572 def subst eqMp 475 ref 70 ref 132 ref 393 ref 481 ref 74 ref 546 ref 78 ref appTerm betaConv 573 def absThm appThm appThm 564 ref appThm appThm 481 ref 74 ref 393 ref 573 remove appThm 564 remove appThm absThm appThm appThm nil "p" 71 ref var 574 def 546 remove nil cons cons 565 remove cons nil cons cons 173 ref 572 ref subst subst eqMp 481 ref 74 ref 132 ref 369 ref 545 ref appTerm 575 def refl 576 def 488 ref 11 ref 551 ref 22 ref appTerm betaConv 577 def absThm appThm appThm appThm 488 ref 11 ref 576 remove 577 remove appThm absThm appThm appThm nil "q" 9 ref var 578 def 551 remove nil cons cons 90 ref 545 remove nil cons 579 def cons 580 def nil cons cons nil cons cons 36 ref 505 ref 39 ref 369 ref 93 ref appTerm 581 def 512 remove appTerm appTerm 69 ref 49 ref 581 remove 508 remove appTerm absTerm appTerm appTerm absTerm 582 def 507 remove appTerm 583 def betaConv 90 ref 349 ref 582 ref appTerm 584 def absTerm 585 def 93 ref appTerm 586 def betaConv nil 230 ref 585 ref appTerm 587 def axiom nil 90 ref 587 remove nil cons cons 91 ref 586 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 251 ref 252 ref 585 remove nil cons cons 291 remove cons nil cons cons 162 ref subst eqMp eqMp nil 90 ref 584 remove nil cons cons 91 ref 583 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 351 ref 352 ref 582 remove nil cons cons 520 remove cons nil cons cons 162 ref subst eqMp eqMp 588 def subst subst eqMp absThm appThm trans absThm appThm trans absThm appThm trans trans trans trans 297 remove assume eqMp nil 90 ref 358 ref 261 ref 69 ref 70 ref 73 ref 74 ref 487 ref 11 ref 575 remove 550 ref appTerm 589 def absTerm 590 def appTerm 591 def absTerm 592 def appTerm 593 def absTerm 594 def appTerm 595 def absTerm 596 def appTerm 597 def nil cons cons 300 ref cons nil cons cons 152 ref subst proveHyp nil 308 ref 261 ref 92 ref 596 ref 262 ref appTerm 598 def appTerm 279 ref appTerm 599 def absTerm nil cons cons nil cons nil cons cons 311 ref 59 ref subst 600 def subst 261 ref nil 61 ref 599 remove nil cons cons nil cons nil cons cons 67 ref subst nil 90 ref 598 ref nil cons 601 def cons 300 ref cons nil cons cons 602 def 109 ref subst 602 remove 160 ref subst 598 ref betaConv 598 remove assume eqMp nil 90 ref 595 ref nil cons cons 300 ref cons nil cons cons 152 ref subst proveHyp nil 44 ref 70 ref 92 ref 594 ref 76 ref appTerm 603 def appTerm 279 ref appTerm 604 def absTerm nil cons cons nil cons nil cons cons 59 ref subst 70 ref nil 61 ref 604 remove nil cons cons nil cons nil cons cons 67 ref subst nil 90 ref 603 ref nil cons 605 def cons 300 ref cons nil cons cons 606 def 109 ref subst 606 remove 160 ref subst 603 ref betaConv 603 remove assume eqMp nil 90 ref 593 ref nil cons cons 300 ref cons nil cons cons 152 ref subst proveHyp nil 168 ref 74 ref 92 ref 592 ref 78 ref appTerm 607 def appTerm 279 ref appTerm 608 def absTerm nil cons cons nil cons nil cons cons 174 ref subst 74 ref nil 61 ref 608 remove nil cons cons nil cons nil cons cons 67 ref subst nil 90 ref 607 ref nil cons 609 def cons 300 ref cons nil cons cons 610 def 109 ref subst 610 remove 160 ref subst 607 ref betaConv 607 remove assume eqMp nil 90 ref 591 ref nil cons cons 300 ref cons nil cons cons 152 ref subst proveHyp nil 10 ref 11 ref 92 ref 590 ref 22 ref appTerm 611 def appTerm 279 ref appTerm 612 def absTerm 613 def nil cons cons nil cons nil cons cons 60 ref subst 11 ref nil 61 ref 612 remove nil cons cons nil cons nil cons cons 67 ref subst nil 90 ref 611 ref nil cons 614 def cons 300 ref cons nil cons cons 615 def 109 ref subst 615 remove 160 ref subst 611 ref betaConv 611 remove assume eqMp nil 90 ref 589 remove nil cons 616 def cons 300 ref cons nil cons cons 617 def 152 ref subst proveHyp 617 ref 109 ref subst 617 remove 160 ref subst nil 90 ref 550 remove nil cons 618 def cons 300 ref cons nil cons cons 619 def 109 ref subst 619 remove 160 ref subst nil "_1323" 6 ref var 620 def 153 ref cons nil cons nil cons cons 31 remove 620 remove varTerm 621 def appTerm 622 def betaConv nil 303 remove 91 ref 622 remove nil cons cons nil cons cons nil cons cons 152 ref subst 34 ref 32 remove 11 ref 621 remove nil cons cons nil cons cons nil cons cons 162 ref subst eqMp eqMp subst 623 def nil 90 ref 62 remove cons 624 def 91 ref 262 ref 28 ref appTerm 625 def nil cons 626 def cons nil cons 627 def cons nil cons cons 160 ref subst proveHyp nil "_1325" 3 ref var 628 def 27 ref nil cons 629 def cons "_1324" 2 ref var 630 def 23 ref nil cons 631 def cons nil cons cons nil cons cons 74 ref 262 ref 17 ref 630 remove varTerm 632 def appTerm 78 ref appTerm appTerm absTerm 633 def 628 remove varTerm 634 def appTerm 635 def betaConv 269 remove 632 ref appTerm 636 def betaConv nil 128 ref 499 remove nil cons cons 130 ref 364 ref cons nil cons cons nil cons cons 637 def 132 ref 136 remove 147 ref appTerm betaConv 147 remove 133 ref appTerm betaConv 138 remove appThm 146 remove 135 ref appTerm betaConv trans trans appThm 148 remove appThm 143 remove 149 remove appThm eqMp sym 66 ref eqMp 638 def subst nil 90 ref 364 ref cons 639 def 91 ref 636 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 195 ref 474 ref 49 ref 632 remove nil cons cons nil cons cons nil cons cons 162 ref subst eqMp eqMp nil 90 ref 189 ref 633 ref appTerm nil cons cons 91 ref 635 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 172 ref 168 ref 633 remove nil cons cons 197 ref 634 remove nil cons cons nil cons cons nil cons cons 162 ref subst eqMp eqMp subst eqMp nil 90 ref 98 ref 30 ref appTerm 640 def 625 remove appTerm nil cons cons 91 ref 263 ref nil cons 641 def cons nil cons 642 def cons nil cons cons 152 ref subst proveHyp nil "_1337" 6 ref var 643 def 153 ref cons "_1336" 6 ref var 644 def 28 ref nil cons 645 def cons nil cons cons nil cons cons nil "b" 7 ref var 646 def 369 ref 275 ref 14 ref 644 remove varTerm 647 def appTerm 643 remove varTerm 648 def appTerm 649 def appTerm 650 def appTerm 275 ref 262 ref 647 remove appTerm 651 def appTerm 652 def appTerm nil cons cons "a" 7 ref var 653 def 262 ref 648 remove appTerm 654 def nil cons 655 def cons nil cons cons nil cons cons nil 90 ref 39 ref 653 ref varTerm 656 def appTerm 657 def 279 ref appTerm 658 def nil cons 659 def cons 660 def 91 ref 39 ref 369 ref 656 ref appTerm 646 ref varTerm 661 def appTerm 662 def appTerm 92 ref 275 ref 661 ref appTerm 663 def appTerm 664 def 656 ref appTerm appTerm nil cons 665 def cons nil cons 666 def cons nil cons cons 667 def 109 ref subst 667 remove 160 ref subst 39 ref "_606" 7 ref var 668 def 39 ref 369 ref 668 remove varTerm 669 def appTerm 661 ref appTerm appTerm 664 ref 669 remove appTerm appTerm absTerm 670 def 656 ref appTerm 671 def appTerm refl 672 def 670 ref 279 ref appTerm betaConv appThm 132 ref 671 remove betaConv appThm 673 def 39 ref 409 remove 661 ref appTerm 674 def appTerm 664 ref 279 ref appTerm appTerm refl appThm trans 670 remove refl 675 def 658 remove assume 676 def appThm eqMp sym 132 ref nil 61 ref 661 ref nil cons 677 def cons nil cons nil cons cons 678 def 413 ref subst 679 def appThm nil 61 ref 663 ref nil cons 680 def cons nil cons nil cons cons 681 def 285 ref subst 678 ref 289 ref subst trans appThm nil 253 ref 677 remove cons nil cons nil cons cons 295 ref subst 682 def trans sym 66 ref eqMp eqMp eqMp nil 128 ref 659 ref cons 683 def 130 ref 665 ref cons nil cons 684 def cons nil cons cons 144 ref subst deductAntisym eqMp nil 90 ref 657 ref 50 ref appTerm 685 def nil cons 686 def cons 687 def 666 remove cons nil cons cons 688 def 109 ref subst 688 remove 160 ref subst 672 remove "_604" 7 ref var 689 def 39 ref 369 ref 689 remove varTerm 690 def appTerm 661 ref appTerm appTerm 664 ref 690 remove appTerm appTerm absTerm 50 ref appTerm betaConv appThm 673 remove 39 ref 369 ref 50 ref appTerm 691 def 661 ref appTerm 692 def appTerm 664 remove 50 ref appTerm appTerm refl appThm trans 675 remove 685 remove assume 693 def appThm eqMp sym 132 ref 678 ref 61 ref 39 ref 691 remove 63 ref appTerm appTerm 50 ref appTerm absTerm 694 def 63 ref appTerm 695 def betaConv nil 230 ref 694 ref appTerm 696 def axiom nil 90 ref 696 remove nil cons cons 91 ref 695 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 251 ref 252 ref 694 remove nil cons cons 284 ref cons nil cons cons 162 ref subst eqMp eqMp 697 def subst 698 def appThm 681 ref 61 ref 39 ref 278 ref 50 ref appTerm appTerm 50 ref appTerm absTerm 699 def 63 ref appTerm 700 def betaConv nil 230 ref 699 ref appTerm 701 def axiom nil 90 ref 701 remove nil cons cons 91 ref 700 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 251 ref 252 ref 699 remove nil cons cons 284 ref cons nil cons cons 162 ref subst eqMp eqMp 702 def subst 703 def appThm nil 61 ref 50 ref nil cons 704 def cons nil cons nil cons cons 705 def 431 ref subst 706 def trans sym 66 ref eqMp eqMp eqMp nil 128 ref 686 remove cons 707 def 684 remove cons nil cons cons 144 ref subst deductAntisym eqMp 442 ref 656 ref appTerm 708 def betaConv 445 ref nil 446 ref 91 ref 708 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 251 ref 447 ref 253 ref 656 ref nil cons 709 def cons nil cons cons nil cons cons 162 ref subst eqMp eqMp 710 def nil 707 ref 130 ref 659 remove cons 711 def 450 ref 665 remove cons nil cons cons cons nil cons cons 469 ref subst proveHyp proveHyp proveHyp 712 def subst 92 ref refl 713 def nil 646 ref 652 ref nil cons 714 def cons 653 ref 650 remove nil cons 715 def cons nil cons cons nil cons cons nil 660 ref 91 ref 39 ref 275 ref 662 remove appTerm appTerm 98 ref 275 ref 656 ref appTerm 716 def appTerm 663 ref appTerm appTerm nil cons 717 def cons nil cons 718 def cons nil cons cons 719 def 109 ref subst 719 remove 160 ref subst 39 ref "_610" 7 ref var 720 def 39 ref 275 ref 369 ref 720 remove varTerm 721 def appTerm 661 ref appTerm appTerm appTerm 98 ref 275 ref 721 remove appTerm appTerm 663 ref appTerm appTerm absTerm 722 def 656 ref appTerm 723 def appTerm refl 724 def 722 ref 279 ref appTerm betaConv appThm 132 ref 723 remove betaConv appThm 725 def 39 ref 275 ref 674 remove appTerm appTerm 384 remove 663 ref appTerm appTerm refl appThm trans 722 remove refl 726 def 676 ref appThm eqMp sym 132 ref 312 ref 679 ref appThm appThm 403 remove 663 ref refl 727 def appThm 681 ref 408 remove subst trans appThm nil 253 ref 680 remove cons nil cons nil cons cons 295 ref subst trans sym 66 ref eqMp eqMp eqMp nil 683 ref 130 ref 717 ref cons nil cons 728 def cons nil cons cons 144 ref subst deductAntisym eqMp nil 687 ref 718 remove cons nil cons cons 729 def 109 ref subst 729 remove 160 ref subst 724 remove "_608" 7 ref var 730 def 39 ref 275 ref 369 ref 730 remove varTerm 731 def appTerm 661 ref appTerm appTerm appTerm 98 ref 275 ref 731 remove appTerm appTerm 663 ref appTerm appTerm absTerm 50 ref appTerm betaConv appThm 725 remove 39 ref 275 ref 692 remove appTerm appTerm 426 remove 663 remove appTerm appTerm refl appThm trans 726 remove 693 ref appThm eqMp sym 132 ref 312 ref 698 ref appThm 434 ref trans appThm 435 remove 727 remove appThm 681 remove 399 remove subst trans appThm nil 61 ref 299 ref cons nil cons nil cons cons 390 ref subst 402 ref trans trans sym 66 ref eqMp eqMp eqMp nil 707 ref 728 remove cons nil cons cons 144 ref subst deductAntisym eqMp 710 ref nil 707 ref 711 ref 450 ref 717 remove cons nil cons cons cons nil cons cons 469 ref subst proveHyp proveHyp proveHyp 732 def subst 400 ref nil 653 ref 649 ref nil cons 733 def cons nil cons 734 def nil cons cons nil 61 ref 709 remove cons nil cons nil cons cons 289 ref subst 735 def subst appThm nil 653 ref 651 ref nil cons cons nil cons 736 def nil cons cons 735 ref subst appThm trans appThm 654 ref refl appThm trans nil 456 ref 714 remove cons 91 ref 655 ref cons 90 ref 715 remove cons nil cons cons cons nil cons cons 132 ref nil "t3" 7 ref var 737 def 457 ref nil cons 738 def cons 739 def "t2" 7 ref var 740 def 124 ref cons "t1" 7 ref var 741 def 121 ref cons nil cons cons 742 def cons nil cons cons 737 ref 39 ref 369 ref 741 ref varTerm 743 def appTerm 744 def 369 ref 740 ref varTerm 745 def appTerm 746 def 737 ref varTerm 747 def appTerm appTerm 748 def appTerm 369 ref 744 remove 745 ref appTerm 749 def appTerm 747 ref appTerm 750 def appTerm 751 def absTerm 752 def 747 ref appTerm 753 def betaConv 740 ref 230 ref 752 ref appTerm 754 def absTerm 755 def 745 ref appTerm 756 def betaConv 741 ref 230 ref 755 ref appTerm 757 def absTerm 758 def 743 ref appTerm 759 def betaConv 230 ref refl 760 def 741 ref 760 ref 740 ref 760 remove 737 ref 751 remove assume sym 39 ref 750 remove appTerm 748 remove appTerm 761 def assume sym deductAntisym absThm appThm absThm appThm absThm appThm nil 230 ref 741 ref 230 ref 740 ref 230 ref 737 remove 761 remove absTerm appTerm absTerm appTerm absTerm appTerm axiom eqMp nil 90 ref 230 ref 758 ref appTerm nil cons cons 91 ref 759 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 251 ref 252 ref 758 remove nil cons cons 253 ref 743 ref nil cons cons nil cons 762 def cons nil cons cons 162 ref subst eqMp eqMp nil 90 ref 757 remove nil cons cons 91 ref 756 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 251 ref 252 ref 755 remove nil cons cons 253 ref 745 ref nil cons cons nil cons 763 def cons nil cons cons 162 ref subst eqMp eqMp nil 90 ref 754 remove nil cons cons 91 ref 753 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 251 ref 252 ref 752 remove nil cons cons 253 ref 747 remove nil cons cons nil cons cons nil cons cons 162 ref subst eqMp eqMp 764 def subst appThm nil 739 remove 740 ref 121 ref cons 741 ref 124 ref cons nil cons cons cons nil cons cons 764 remove subst appThm sym 393 ref nil 742 remove nil cons cons 740 remove 39 ref 749 remove appTerm 746 remove 743 ref appTerm appTerm absTerm 765 def 745 remove appTerm 766 def betaConv 741 remove 230 ref 765 ref appTerm 767 def absTerm 768 def 743 remove appTerm 769 def betaConv nil 230 ref 768 ref appTerm 770 def axiom nil 90 ref 770 remove nil cons cons 91 ref 769 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 251 ref 252 ref 768 remove nil cons cons 762 remove cons nil cons cons 162 ref subst eqMp eqMp nil 90 ref 767 remove nil cons cons 91 ref 766 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 251 ref 252 ref 765 remove nil cons cons 763 remove cons nil cons cons 162 ref subst eqMp eqMp subst 771 def appThm 457 remove refl appThm eqMp 772 def subst nil 646 ref 369 ref 654 ref appTerm 652 remove appTerm nil cons 773 def cons 734 remove cons nil cons cons nil 660 ref 91 ref 39 ref 92 ref 656 ref appTerm 661 ref appTerm appTerm 369 ref 716 ref appTerm 661 ref appTerm appTerm nil cons 774 def cons nil cons 775 def cons nil cons cons 776 def 109 ref subst 776 remove 160 ref subst 39 ref "_630" 7 ref var 777 def 39 ref 92 ref 777 remove varTerm 778 def appTerm 661 ref appTerm appTerm 369 ref 275 ref 778 remove appTerm appTerm 661 ref appTerm appTerm absTerm 779 def 656 ref appTerm 780 def appTerm refl 781 def 779 ref 279 ref appTerm betaConv appThm 132 ref 780 remove betaConv appThm 782 def 39 ref 92 ref 279 ref appTerm 783 def 661 ref appTerm appTerm 369 ref 383 ref appTerm 784 def 661 ref appTerm appTerm refl appThm trans 779 remove refl 785 def 676 ref appThm eqMp sym 132 ref 678 ref 61 ref 39 ref 783 ref 63 ref appTerm appTerm 50 ref appTerm absTerm 786 def 63 ref appTerm 787 def betaConv nil 230 ref 786 ref appTerm 788 def axiom nil 90 ref 788 remove nil cons cons 91 ref 787 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 251 ref 252 ref 786 remove nil cons cons 284 ref cons nil cons cons 162 ref subst eqMp eqMp subst appThm 393 ref 402 ref appThm 661 ref refl 789 def appThm 698 remove trans appThm 706 remove trans sym 66 ref eqMp eqMp eqMp nil 683 ref 130 ref 774 ref cons nil cons 790 def cons nil cons cons 144 ref subst deductAntisym eqMp nil 687 ref 775 remove cons nil cons cons 791 def 109 ref subst 791 remove 160 ref subst 781 remove "_628" 7 ref var 792 def 39 ref 92 ref 792 remove varTerm 793 def appTerm 661 ref appTerm appTerm 369 ref 275 ref 793 remove appTerm appTerm 661 ref appTerm appTerm absTerm 50 ref appTerm betaConv appThm 782 remove 39 ref 92 ref 50 ref appTerm 794 def 661 ref appTerm appTerm 369 ref 425 ref appTerm 795 def 661 ref appTerm appTerm refl appThm trans 785 remove 693 ref appThm eqMp sym 132 ref 678 ref 61 ref 39 ref 794 remove 63 ref appTerm appTerm 63 ref appTerm absTerm 796 def 63 ref appTerm 797 def betaConv nil 230 ref 796 ref appTerm 798 def axiom nil 90 ref 798 remove nil cons cons 91 ref 797 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 251 ref 252 ref 796 remove nil cons cons 284 ref cons nil cons cons 162 ref subst eqMp eqMp subst appThm 393 ref 434 ref appThm 789 remove appThm 679 remove trans appThm 682 remove trans sym 66 ref eqMp eqMp eqMp nil 707 ref 790 remove cons nil cons cons 144 ref subst deductAntisym eqMp 710 ref nil 707 ref 711 ref 450 ref 774 remove cons nil cons cons cons nil cons cons 469 ref subst proveHyp proveHyp proveHyp 799 def subst nil 90 ref 733 ref cons 91 ref 773 ref cons nil cons 800 def cons nil cons cons 801 def 109 ref subst 801 remove 160 ref subst 262 ref refl 802 def 649 remove assume appThm nil 90 ref 39 ref 651 remove appTerm 654 remove appTerm nil cons cons 800 remove cons nil cons cons 152 ref subst proveHyp nil 646 ref 655 remove cons 736 remove cons nil cons cons nil 660 remove 91 ref 92 ref 657 remove 661 ref appTerm appTerm 369 ref 661 ref appTerm 803 def 716 remove appTerm appTerm nil cons 804 def cons nil cons 805 def cons nil cons cons 806 def 109 ref subst 806 remove 160 ref subst 39 ref "_634" 7 ref var 807 def 92 ref 39 ref 807 remove varTerm 808 def appTerm 661 ref appTerm appTerm 803 ref 275 ref 808 remove appTerm appTerm appTerm absTerm 809 def 656 remove appTerm 810 def appTerm refl 811 def 809 ref 279 ref appTerm betaConv appThm 132 ref 810 remove betaConv appThm 812 def 92 ref 380 ref 661 ref appTerm appTerm 803 ref 383 ref appTerm appTerm refl appThm trans 809 remove refl 813 def 676 remove appThm eqMp sym 713 ref 678 ref 390 ref subst appThm 803 ref refl 814 def 402 ref appThm 678 ref 61 ref 39 ref 436 ref 50 ref appTerm appTerm 50 ref appTerm absTerm 815 def 63 ref appTerm 816 def betaConv nil 230 ref 815 ref appTerm 817 def axiom nil 90 ref 817 remove nil cons cons 91 ref 816 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 251 ref 252 ref 815 remove nil cons cons 284 ref cons nil cons cons 162 ref subst eqMp eqMp 818 def subst trans appThm 703 remove trans sym 66 ref eqMp eqMp eqMp nil 683 remove 130 ref 804 ref cons nil cons 819 def cons nil cons cons 144 ref subst deductAntisym eqMp nil 687 remove 805 remove cons nil cons cons 820 def 109 ref subst 820 remove 160 ref subst 811 remove "_632" 7 ref var 821 def 92 ref 39 ref 821 remove varTerm 822 def appTerm 661 ref appTerm appTerm 803 ref 275 ref 822 remove appTerm appTerm appTerm absTerm 50 ref appTerm betaConv appThm 812 remove 92 ref 423 ref 661 remove appTerm appTerm 803 remove 425 ref appTerm appTerm refl appThm trans 813 remove 693 remove appThm eqMp sym 713 ref 678 ref 431 ref subst appThm 814 remove 434 ref appThm 678 ref 440 ref subst trans appThm 678 remove nil 61 ref 278 remove 63 ref appTerm 823 def nil cons cons nil cons nil cons cons 67 ref subst 61 ref 823 remove absTerm 824 def 63 ref appTerm 825 def betaConv nil 230 ref 824 ref appTerm 826 def axiom nil 90 ref 826 remove nil cons cons 91 ref 825 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 251 ref 252 ref 824 remove nil cons cons 284 ref cons nil cons cons 162 ref subst eqMp eqMp eqMp 827 def subst trans sym 66 ref eqMp eqMp eqMp nil 707 ref 819 remove cons nil cons cons 144 ref subst deductAntisym eqMp 710 remove nil 707 remove 711 remove 450 ref 804 remove cons nil cons cons cons nil cons cons 469 ref subst proveHyp proveHyp proveHyp 828 def subst eqMp eqMp nil 128 ref 733 remove cons 130 ref 773 remove cons nil cons cons nil cons cons 144 ref subst deductAntisym eqMp eqMp eqMp eqMp subst eqMp nil 90 ref 641 ref cons 829 def 300 ref cons nil cons cons 152 ref subst proveHyp nil 829 remove nil cons nil cons cons 39 ref 276 remove appTerm 830 def refl 122 remove 285 remove subst appThm nil 253 ref 277 remove cons nil cons nil cons cons 295 ref subst trans sym 66 ref eqMp 831 def subst 637 remove 144 ref subst eqMp eqMp eqMp nil 128 ref 618 ref cons 130 ref 299 ref cons nil cons 832 def cons nil cons cons 144 ref subst deductAntisym eqMp nil 580 remove 300 ref cons nil cons cons 833 def 109 ref subst 833 remove 160 ref subst nil "_1322" 6 ref var 834 def 79 ref nil cons 835 def cons nil cons nil cons cons 264 ref 834 remove varTerm 836 def appTerm 837 def betaConv nil 128 ref 362 ref cons 130 ref 494 remove nil cons cons nil cons cons nil cons cons 838 def 144 ref subst nil 363 remove 91 ref 837 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 34 ref 485 remove 11 ref 836 remove nil cons cons nil cons cons nil cons cons 162 ref subst eqMp eqMp subst nil 90 ref 266 ref nil cons 839 def cons 840 def 300 ref cons nil cons cons 152 ref subst 841 def proveHyp nil 840 remove nil cons nil cons cons 831 ref subst 838 remove 638 ref subst eqMp eqMp eqMp nil 128 ref 579 remove cons 842 def 832 ref cons nil cons cons 144 ref subst deductAntisym eqMp nil 842 remove 130 ref 618 remove cons 450 ref 299 ref cons nil cons 843 def cons cons nil cons cons 469 ref subst proveHyp proveHyp eqMp nil 128 ref 616 remove cons 832 ref cons nil cons cons 144 ref subst deductAntisym eqMp eqMp eqMp nil 128 ref 614 remove cons 832 ref cons nil cons cons 144 ref subst deductAntisym eqMp eqMp absThm eqMp nil 90 ref 88 ref 613 remove appTerm nil cons cons 91 ref 92 ref 591 remove appTerm 279 ref appTerm nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 34 ref 10 ref 590 remove nil cons cons 832 ref cons nil cons cons 256 ref subst eqMp eqMp eqMp nil 128 ref 609 remove cons 832 ref cons nil cons cons 144 ref subst deductAntisym eqMp eqMp absThm eqMp nil 90 ref 189 ref 197 ref 92 ref 592 ref 211 ref appTerm appTerm 279 ref appTerm absTerm appTerm nil cons cons 91 ref 92 ref 593 remove appTerm 279 ref appTerm nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 172 ref 168 ref 592 remove nil cons cons 832 ref cons nil cons cons 256 ref subst eqMp eqMp eqMp nil 128 ref 605 remove cons 832 ref cons nil cons cons 144 ref subst deductAntisym eqMp eqMp absThm eqMp nil 90 ref 43 ref 49 ref 92 ref 594 ref 156 ref appTerm appTerm 279 ref appTerm absTerm appTerm nil cons cons 91 ref 92 ref 595 remove appTerm 279 ref appTerm nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 195 ref 44 ref 594 remove nil cons cons 832 ref cons nil cons cons 256 ref subst eqMp eqMp eqMp nil 128 ref 601 remove cons 832 ref cons nil cons cons 144 ref subst deductAntisym eqMp eqMp absThm eqMp nil 90 ref 260 ref "x" 9 ref var 844 def 92 ref 596 ref 844 ref varTerm 845 def appTerm appTerm 279 ref appTerm absTerm appTerm nil cons cons 91 ref 92 ref 597 remove appTerm 279 ref appTerm nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 310 ref 308 ref 596 remove nil cons cons 832 ref cons nil cons cons 256 ref subst eqMp eqMp eqMp nil 128 ref 302 remove cons 832 ref cons nil cons cons 144 ref subst 846 def deductAntisym eqMp eqMp eqMp nil 128 ref 298 remove cons 832 ref cons nil cons cons 144 ref subst deductAntisym eqMp eqMp 847 def nil 272 remove thm nil 90 ref 260 ref 261 ref 39 ref 487 ref 264 remove appTerm 848 def appTerm 69 ref 70 ref 73 ref 267 remove appTerm absTerm 849 def appTerm 850 def appTerm absTerm 851 def appTerm 852 def nil cons cons 853 def nil cons nil cons cons 296 ref subst sym nil 90 ref 275 ref 852 ref appTerm 854 def nil cons 855 def cons 300 ref cons nil cons cons 856 def 109 ref subst 856 remove 160 ref subst 305 remove 306 remove 307 remove nil 308 ref 851 ref nil cons cons 857 def nil cons nil cons cons 357 remove subst 359 ref 261 ref 312 ref 851 remove 262 ref appTerm 858 def betaConv 859 def appThm nil 90 ref 848 ref nil cons cons 91 ref 850 ref nil cons cons nil cons cons nil cons cons 470 ref subst 393 ref 400 ref 488 ref 472 remove appThm appThm nil 44 ref 849 ref nil cons 860 def cons nil cons nil cons cons 132 ref 312 ref 475 ref 341 remove appThm appThm appThm 43 ref 342 remove appTerm refl appThm sym 343 remove 47 ref 39 ref 275 ref 510 ref appTerm appTerm 43 ref 346 ref appTerm 861 def appTerm absTerm 862 def 48 ref appTerm 863 def betaConv nil 349 ref 862 ref appTerm 864 def axiom 865 def nil 90 ref 864 remove nil cons cons 91 ref 863 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 351 ref 352 ref 862 remove nil cons cons 355 ref cons nil cons cons 162 ref subst eqMp eqMp 866 def subst eqMp 867 def subst 313 ref 70 ref 312 ref 849 remove 76 ref appTerm betaConv 868 def appThm 480 remove 173 ref 867 ref subst subst 490 ref 484 remove appThm trans trans absThm appThm trans appThm appThm 400 ref 486 ref 36 ref 867 remove subst subst 471 ref 489 remove appThm trans appThm 475 ref 70 ref 481 ref 491 remove appThm absThm appThm appThm appThm trans trans absThm appThm trans 132 ref 359 ref 261 ref 393 ref 261 ref 98 ref 848 remove appTerm 43 ref 70 ref 189 ref 495 remove appTerm absTerm 869 def appTerm 870 def appTerm absTerm 871 def 262 ref appTerm betaConv 872 def appThm 261 ref 98 ref 88 ref 500 ref appTerm 873 def appTerm 874 def 850 remove appTerm absTerm 875 def 262 ref appTerm betaConv 876 def appThm absThm appThm appThm 393 ref 359 ref 261 ref 872 remove absThm appThm appThm 359 ref 261 ref 876 remove absThm appThm appThm appThm nil 503 ref 871 remove nil cons cons 504 ref 875 remove nil cons cons nil cons cons nil cons cons 521 remove subst eqMp 393 ref 359 ref 261 ref nil 91 ref 870 ref nil cons 877 def cons nil cons nil cons cons 544 remove subst absThm appThm appThm 359 ref 261 ref 132 ref 874 ref refl 878 def 475 ref 70 ref 868 ref absThm appThm appThm appThm 475 ref 70 ref 878 ref 868 remove appThm absThm appThm appThm nil 505 ref 860 remove cons 90 ref 873 remove nil cons 879 def cons 880 def nil cons 881 def cons nil cons cons 530 ref subst eqMp 475 ref 70 ref 132 ref 878 ref 481 ref 74 ref 483 ref absThm appThm appThm appThm 481 ref 74 ref 878 remove 483 ref appThm absThm appThm appThm nil 532 ref 478 remove cons 881 remove cons nil cons cons 533 remove subst eqMp absThm appThm trans absThm appThm appThm 132 ref 393 ref 359 ref 261 ref 261 ref 487 ref 11 ref 98 ref 263 ref appTerm 870 remove appTerm 882 def absTerm 883 def appTerm absTerm 884 def 262 ref appTerm betaConv 885 def absThm appThm appThm 359 ref 261 ref 261 ref 69 ref 70 ref 73 ref 74 ref 874 remove 266 remove appTerm 886 def absTerm 887 def appTerm absTerm 888 def appTerm 889 def absTerm 890 def 262 ref appTerm betaConv 891 def absThm appThm appThm appThm 359 ref 261 ref 393 ref 885 remove appThm 891 remove appThm absThm appThm appThm nil 503 ref 884 remove nil cons cons 504 remove 890 remove nil cons cons nil cons cons nil cons cons 562 remove subst eqMp 359 remove 261 ref 132 ref 393 ref 488 ref 11 ref 883 ref 22 ref appTerm betaConv 892 def absThm appThm appThm 889 ref refl 893 def appThm appThm 488 ref 11 ref 393 ref 892 remove appThm 893 remove appThm absThm appThm appThm nil 261 ref 883 remove nil cons cons 91 ref 889 remove nil cons cons nil cons cons nil cons cons 36 ref 572 remove subst subst eqMp 488 ref 11 ref 132 ref 369 ref 882 ref appTerm 894 def refl 895 def 475 ref 70 ref 888 ref 76 ref appTerm betaConv 896 def absThm appThm appThm appThm 475 ref 70 ref 895 ref 896 remove appThm absThm appThm appThm nil 505 ref 888 remove nil cons cons 90 ref 882 remove nil cons 897 def cons 898 def nil cons 899 def cons nil cons cons 588 ref subst eqMp 475 ref 70 ref 132 ref 895 ref 481 ref 74 ref 887 ref 78 ref appTerm betaConv 900 def absThm appThm appThm appThm 481 ref 74 ref 895 remove 900 remove appThm absThm appThm appThm nil 532 remove 887 remove nil cons cons 899 remove cons nil cons cons 173 ref 588 remove subst subst eqMp absThm appThm trans absThm appThm trans absThm appThm trans trans trans trans 854 remove assume eqMp nil 90 ref 358 ref 261 ref 487 ref 11 ref 69 ref 70 ref 73 ref 74 ref 894 remove 886 ref appTerm 901 def absTerm 902 def appTerm 903 def absTerm 904 def appTerm 905 def absTerm 906 def appTerm 907 def absTerm 908 def appTerm 909 def nil cons cons 300 ref cons nil cons cons 152 ref subst proveHyp nil 308 ref 261 ref 92 ref 908 ref 262 ref appTerm 910 def appTerm 279 ref appTerm 911 def absTerm nil cons cons nil cons nil cons cons 600 ref subst 261 ref nil 61 ref 911 remove nil cons cons nil cons nil cons cons 67 ref subst nil 90 ref 910 ref nil cons 912 def cons 300 ref cons nil cons cons 913 def 109 ref subst 913 remove 160 ref subst 910 ref betaConv 910 remove assume eqMp nil 90 ref 907 ref nil cons cons 300 ref cons nil cons cons 152 ref subst proveHyp nil 10 ref 11 ref 92 ref 906 ref 22 ref appTerm 914 def appTerm 279 ref appTerm 915 def absTerm 916 def nil cons cons nil cons nil cons cons 60 ref subst 11 ref nil 61 ref 915 remove nil cons cons nil cons nil cons cons 67 ref subst nil 90 ref 914 ref nil cons 917 def cons 300 ref cons nil cons cons 918 def 109 ref subst 918 remove 160 ref subst 914 ref betaConv 914 remove assume eqMp nil 90 ref 905 ref nil cons cons 300 ref cons nil cons cons 152 ref subst proveHyp nil 44 ref 70 ref 92 ref 904 ref 76 ref appTerm 919 def appTerm 279 ref appTerm 920 def absTerm nil cons cons nil cons nil cons cons 59 ref subst 70 ref nil 61 ref 920 remove nil cons cons nil cons nil cons cons 67 ref subst nil 90 ref 919 ref nil cons 921 def cons 300 ref cons nil cons cons 922 def 109 ref subst 922 remove 160 ref subst 919 ref betaConv 919 remove assume eqMp nil 90 ref 903 ref nil cons cons 300 ref cons nil cons cons 152 ref subst proveHyp nil 168 ref 74 ref 92 ref 902 ref 78 ref appTerm 923 def appTerm 279 ref appTerm 924 def absTerm nil cons cons nil cons nil cons cons 174 ref subst 74 ref nil 61 ref 924 remove nil cons cons nil cons nil cons cons 67 ref subst nil 90 ref 923 ref nil cons 925 def cons 300 ref cons nil cons cons 926 def 109 ref subst 926 remove 160 ref subst 923 ref betaConv 923 remove assume eqMp nil 90 ref 901 remove nil cons 927 def cons 300 ref cons nil cons cons 928 def 152 ref subst proveHyp 928 ref 109 ref subst 928 remove 160 ref subst nil 90 ref 886 remove nil cons 929 def cons 300 ref cons nil cons cons 930 def 109 ref subst 930 remove 160 ref subst nil 128 ref 879 remove cons 130 ref 839 remove cons nil cons cons nil cons cons 931 def 638 ref subst 841 remove proveHyp nil "_1350" 6 ref var 932 def 835 ref cons nil cons nil cons cons nil 90 ref 262 ref 932 remove varTerm 933 def appTerm nil cons cons nil cons nil cons cons 831 ref subst 500 remove 933 ref appTerm 934 def betaConv 931 remove 144 ref subst nil 880 remove 91 ref 934 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 34 ref 10 ref 535 remove cons 11 ref 933 remove nil cons cons nil cons cons nil cons cons 162 ref subst eqMp eqMp eqMp subst eqMp eqMp nil 128 ref 929 ref cons 832 ref cons nil cons cons 144 ref subst deductAntisym eqMp nil 898 remove 300 ref cons nil cons cons 935 def 109 ref subst 935 remove 160 ref subst 623 remove nil 624 remove 91 ref 29 remove 28 ref appTerm 936 def nil cons cons nil cons cons nil cons cons 160 ref subst proveHyp nil 11 ref 645 ref cons nil cons 937 def nil cons cons 36 ref 161 remove subst subst eqMp nil 90 ref 640 remove 936 remove appTerm nil cons cons 91 ref 75 ref 28 remove appTerm 938 def nil cons 939 def cons nil cons cons nil cons cons 152 ref subst proveHyp nil "z" 6 ref var 940 def 645 ref cons "y" 6 ref var 941 def 153 ref cons 937 remove cons cons nil cons cons nil 646 ref 369 ref 275 ref 75 ref 941 ref varTerm 942 def appTerm 943 def appTerm 944 def appTerm 945 def 275 ref 75 remove 940 ref varTerm 946 def appTerm 947 def appTerm 948 def appTerm nil cons cons 653 ref 14 ref 942 remove appTerm 946 ref appTerm 949 def nil cons 950 def cons nil cons cons nil cons cons 712 ref subst 713 ref nil 646 ref 948 remove nil cons 951 def cons 653 ref 944 remove nil cons 952 def cons nil cons cons nil cons cons 732 ref subst 400 ref nil 653 ref 943 remove nil cons cons nil cons nil cons cons 735 ref subst appThm nil 653 ref 947 remove nil cons cons nil cons nil cons cons 735 ref subst appThm trans appThm 949 remove refl appThm trans 945 remove refl nil 91 ref 950 remove cons 953 def 90 ref 951 ref cons nil cons cons nil cons cons 771 remove subst appThm nil 456 ref 951 remove cons 953 remove 90 ref 952 remove cons nil cons cons cons nil cons cons 772 ref subst trans 36 ref nil 90 ref 275 ref 293 ref "y" 2 ref var 954 def varTerm 955 def appTerm 956 def appTerm 957 def nil cons 958 def cons 959 def 91 ref 369 ref 957 remove appTerm 369 ref 275 ref 293 remove "z" 2 ref var varTerm 960 def appTerm appTerm appTerm 186 ref 955 ref appTerm 961 def 960 ref appTerm 962 def appTerm 963 def appTerm nil cons 964 def cons nil cons 965 def cons nil cons cons 966 def 109 ref subst 966 remove 160 ref subst 393 ref 312 ref nil 959 remove 91 ref 39 ref 956 ref appTerm 967 def 279 ref appTerm nil cons cons nil cons cons nil cons cons 152 ref subst nil 128 ref 956 ref nil cons 968 def cons 969 def nil cons nil cons cons nil 90 ref 275 ref 133 ref appTerm 970 def nil cons 971 def cons 91 ref 39 ref 133 ref appTerm 279 ref appTerm nil cons 972 def cons nil cons cons nil cons cons 973 def 109 ref subst 973 remove 160 ref subst nil 90 ref 133 ref nil cons 974 def cons 300 ref cons nil cons cons 247 remove nil 90 ref 243 ref cons 975 def 91 ref 463 ref 93 ref appTerm nil cons 976 def cons nil cons 977 def cons nil cons cons 160 ref subst proveHyp 463 ref refl 246 remove appThm sym nil 90 ref 124 ref cons 978 def 91 ref 124 ref cons nil cons 979 def cons nil cons cons 980 def 109 ref subst 980 remove 160 ref subst 126 remove eqMp nil 128 ref 124 remove cons 131 ref cons nil cons cons 144 ref subst deductAntisym eqMp eqMp 981 def eqMp nil 978 ref 91 ref 121 ref cons nil cons 982 def cons nil cons cons 152 ref subst nil 128 ref 243 remove cons 983 def 130 ref 976 remove cons nil cons 984 def cons nil cons cons 985 def 638 ref subst eqMp 152 ref 985 remove 144 ref subst eqMp deductAntisym deductAntisym 986 def subst 39 ref 970 ref appTerm refl 90 ref 94 ref 279 ref appTerm absTerm 987 def 133 ref appTerm betaConv appThm nil 117 remove 275 ref appTerm 987 remove appTerm axiom 142 remove appThm eqMp 970 remove assume eqMp nil 90 ref 455 remove 279 ref appTerm nil cons cons 91 ref 783 remove 133 ref appTerm nil cons cons nil cons cons nil cons cons 160 ref subst proveHyp nil 90 ref 299 ref cons 91 ref 974 ref cons nil cons cons nil cons cons 988 def 109 ref subst 988 remove 160 ref subst 90 ref 93 ref absTerm 989 def 133 remove appTerm 990 def betaConv nil 380 ref 230 ref 989 ref appTerm 991 def appTerm axiom 279 ref assume eqMp nil 90 ref 991 remove nil cons cons 91 ref 990 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 251 ref 252 ref 989 remove nil cons cons 253 ref 974 ref cons nil cons cons nil cons cons 162 ref subst eqMp eqMp eqMp nil 128 ref 299 remove cons 130 ref 974 remove cons nil cons cons nil cons cons 144 ref subst deductAntisym eqMp eqMp eqMp eqMp nil 128 ref 971 remove cons 130 ref 972 remove cons nil cons cons nil cons cons 144 ref subst deductAntisym eqMp subst eqMp appThm 402 ref trans appThm 963 ref refl appThm nil 61 ref 963 remove nil cons cons nil cons nil cons cons 697 remove subst trans sym 66 ref eqMp eqMp nil 128 ref 958 ref cons 130 ref 964 ref cons nil cons 992 def cons nil cons cons 144 ref subst deductAntisym eqMp nil 90 ref 968 ref cons 965 remove cons nil cons cons 993 def 109 ref subst 993 remove 160 ref subst 393 ref 312 ref 186 ref refl 956 ref assume appThm 994 def 955 ref refl appThm nil 49 ref 955 ref nil cons cons nil cons 995 def nil cons cons 294 ref subst trans appThm 434 ref trans appThm 393 ref 312 ref 994 remove 960 remove refl appThm appThm appThm 962 ref refl appThm appThm nil 61 ref 369 ref 275 ref 962 ref appTerm appTerm 962 ref appTerm nil cons 996 def cons nil cons nil cons cons 413 remove subst trans sym nil 90 ref 39 ref 962 ref appTerm 997 def 279 ref appTerm 998 def nil cons 999 def cons 91 ref 996 ref cons nil cons 1000 def cons nil cons cons 1001 def 109 ref subst 1001 remove 160 ref subst 39 ref "_626" 7 ref var 1002 def 369 ref 275 ref 1002 remove varTerm 1003 def appTerm appTerm 1003 remove appTerm absTerm 1004 def 962 ref appTerm 1005 def appTerm refl 1006 def 1004 ref 279 ref appTerm betaConv appThm 132 ref 1005 remove betaConv appThm 1007 def 784 remove 279 ref appTerm refl appThm trans 1004 remove refl 1008 def 998 remove assume appThm eqMp sym nil 61 ref 383 remove nil cons cons nil cons nil cons cons 440 remove subst 402 ref trans sym 66 ref eqMp eqMp eqMp nil 128 ref 999 ref cons 130 ref 996 ref cons nil cons 1009 def cons nil cons cons 144 ref subst deductAntisym eqMp nil 90 ref 997 remove 50 ref appTerm 1010 def nil cons 1011 def cons 1000 remove cons nil cons cons 1012 def 109 ref subst 1012 remove 160 ref subst 1006 remove "_624" 7 ref var 1013 def 369 ref 275 ref 1013 remove varTerm 1014 def appTerm appTerm 1014 remove appTerm absTerm 50 ref appTerm betaConv appThm 1007 remove 795 remove 50 ref appTerm refl appThm trans 1008 remove 1010 remove assume appThm eqMp sym nil 61 ref 425 remove nil cons cons nil cons nil cons cons 818 remove subst sym 66 ref eqMp eqMp eqMp nil 128 ref 1011 remove cons 1015 def 1009 remove cons nil cons cons 144 ref subst deductAntisym eqMp 442 ref 962 ref appTerm 1016 def betaConv 445 ref nil 446 ref 91 ref 1016 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 251 ref 447 ref 253 ref 962 remove nil cons cons nil cons cons nil cons cons 162 ref subst eqMp eqMp nil 1015 remove 130 ref 999 remove cons 450 ref 996 remove cons nil cons cons cons nil cons cons 469 ref subst proveHyp proveHyp proveHyp eqMp eqMp nil 969 ref 992 remove cons nil cons cons 144 ref subst deductAntisym eqMp 61 ref 436 remove 280 remove appTerm absTerm 1017 def 956 remove appTerm 1018 def betaConv nil 230 ref 1017 ref appTerm 1019 def axiom nil 90 ref 1019 remove nil cons cons 91 ref 1018 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 251 ref 252 ref 1017 remove nil cons cons 253 ref 968 remove cons nil cons cons nil cons cons 162 ref subst eqMp eqMp nil 969 remove 130 ref 958 remove cons 450 ref 964 remove cons nil cons cons cons nil cons cons 469 ref subst proveHyp proveHyp proveHyp subst eqMp eqMp subst eqMp nil 90 ref 939 remove cons 642 remove cons nil cons cons 160 ref subst proveHyp nil 128 ref 641 ref cons 130 ref 877 ref cons nil cons cons nil cons cons 1020 def 144 ref subst eqMp nil 90 ref 98 ref 938 ref appTerm 263 remove appTerm nil cons cons 627 remove cons nil cons cons 152 ref subst proveHyp nil "_1352" 6 ref var 1021 def 645 remove cons "_1351" 6 ref var 1022 def 153 remove cons nil cons cons nil cons cons nil 646 ref 369 ref 275 ref 14 ref 1022 remove varTerm 1023 def appTerm 1021 remove varTerm 1024 def appTerm 1025 def appTerm 1026 def appTerm 275 ref 262 ref 1023 remove appTerm 1027 def appTerm 1028 def appTerm nil cons cons 653 ref 262 ref 1024 remove appTerm 1029 def nil cons 1030 def cons nil cons cons nil cons cons 712 remove subst 713 ref nil 646 ref 1028 ref nil cons 1031 def cons 653 ref 1026 remove nil cons 1032 def cons nil cons cons nil cons cons 732 remove subst 400 ref nil 653 ref 1025 ref nil cons 1033 def cons nil cons 1034 def nil cons cons 735 ref subst appThm nil 653 remove 1027 ref nil cons cons nil cons 1035 def nil cons cons 735 remove subst appThm trans appThm 1029 ref refl appThm trans nil 456 ref 1031 remove cons 91 ref 1030 ref cons 90 ref 1032 remove cons nil cons cons cons nil cons cons 772 remove subst nil 646 ref 369 ref 1029 ref appTerm 1028 remove appTerm nil cons 1036 def cons 1034 remove cons nil cons cons 799 remove subst nil 90 ref 1033 ref cons 91 ref 1036 ref cons nil cons 1037 def cons nil cons cons 1038 def 109 ref subst 1038 remove 160 ref subst 802 ref 1025 remove assume appThm nil 90 ref 39 ref 1027 remove appTerm 1029 remove appTerm nil cons cons 1037 remove cons nil cons cons 152 ref subst proveHyp nil 646 remove 1030 remove cons 1035 remove cons nil cons cons 828 remove subst eqMp eqMp nil 128 ref 1033 remove cons 130 ref 1036 remove cons nil cons cons nil cons cons 144 ref subst deductAntisym eqMp eqMp eqMp eqMp subst eqMp nil 90 ref 626 remove cons 300 ref cons nil cons cons 152 ref subst proveHyp nil "_1348" 3 ref var 1039 def 629 ref cons "_1347" 2 ref var 1040 def 631 ref cons nil cons cons nil cons cons nil 90 ref 262 ref 17 ref 1040 remove varTerm 1041 def appTerm 1042 def 1039 remove varTerm 1043 def appTerm appTerm nil cons cons nil cons nil cons cons 831 ref subst 74 ref 275 ref 262 ref 1042 remove 78 ref appTerm appTerm appTerm absTerm 1044 def 1043 ref appTerm 1045 def betaConv 869 ref 1041 ref appTerm 1046 def betaConv 1020 remove 638 ref subst nil 90 ref 877 remove cons 91 ref 1046 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 195 ref 44 ref 869 remove nil cons cons 49 ref 1041 remove nil cons cons nil cons cons nil cons cons 162 ref subst eqMp eqMp nil 90 ref 189 ref 1044 ref appTerm nil cons cons 91 ref 1045 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 172 ref 168 ref 1044 remove nil cons cons 197 ref 1043 remove nil cons cons nil cons cons nil cons cons 162 ref subst eqMp eqMp eqMp subst eqMp eqMp nil 128 ref 897 remove cons 1047 def 832 ref cons nil cons cons 144 ref subst deductAntisym eqMp nil 1047 remove 130 ref 929 remove cons 843 ref cons cons nil cons cons 469 ref subst proveHyp proveHyp eqMp nil 128 ref 927 remove cons 832 ref cons nil cons cons 144 ref subst deductAntisym eqMp eqMp eqMp nil 128 ref 925 remove cons 832 ref cons nil cons cons 144 ref subst deductAntisym eqMp eqMp absThm eqMp nil 90 ref 189 ref 197 ref 92 ref 902 ref 211 ref appTerm appTerm 279 ref appTerm absTerm appTerm nil cons cons 91 ref 92 ref 903 remove appTerm 279 ref appTerm nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 172 ref 168 ref 902 remove nil cons cons 832 ref cons nil cons cons 256 ref subst eqMp eqMp eqMp nil 128 ref 921 remove cons 832 ref cons nil cons cons 144 ref subst deductAntisym eqMp eqMp absThm eqMp nil 90 ref 43 ref 49 ref 92 ref 904 ref 156 ref appTerm appTerm 279 ref appTerm absTerm appTerm nil cons cons 91 ref 92 ref 905 remove appTerm 279 ref appTerm nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 195 ref 44 ref 904 remove nil cons cons 832 ref cons nil cons cons 256 ref subst eqMp eqMp eqMp nil 128 ref 917 remove cons 832 ref cons nil cons cons 144 ref subst deductAntisym eqMp eqMp absThm eqMp nil 90 ref 88 ref 916 remove appTerm nil cons cons 91 ref 92 ref 907 remove appTerm 279 ref appTerm nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 34 ref 10 ref 906 remove nil cons cons 832 ref cons nil cons cons 256 ref subst eqMp eqMp eqMp nil 128 ref 912 remove cons 832 ref cons nil cons cons 144 ref subst deductAntisym eqMp eqMp absThm eqMp nil 90 ref 260 ref 844 ref 92 ref 908 ref 845 remove appTerm appTerm 279 ref appTerm absTerm appTerm nil cons cons 91 ref 92 ref 909 remove appTerm 279 ref appTerm nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 310 ref 308 ref 908 remove nil cons cons 832 ref cons nil cons cons 256 ref subst eqMp eqMp eqMp 846 remove deductAntisym eqMp eqMp eqMp nil 128 ref 855 remove cons 832 ref cons nil cons cons 144 ref subst deductAntisym eqMp eqMp 1048 def nil 852 remove thm nil 308 ref 261 ref 92 ref 270 remove appTerm 265 remove appTerm 1049 def absTerm 1050 def nil cons cons nil cons nil cons cons 600 ref subst 261 ref nil 61 ref 1049 remove nil cons cons nil cons nil cons cons 67 ref subst nil 639 ref 91 ref 362 ref cons nil cons cons nil cons cons 1051 def 109 ref subst 1051 remove 160 ref subst 486 remove 60 ref subst 11 ref nil 61 ref 641 remove cons nil cons nil cons cons 67 ref subst 802 remove 11 ref 938 ref absTerm 1052 def 22 ref appTerm 1053 def betaConv 471 ref 11 ref 938 remove assume sym 30 remove assume sym deductAntisym absThm appThm 257 remove eqMp nil 90 ref 88 ref 1052 ref appTerm nil cons cons 91 ref 1053 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 34 ref 10 ref 1052 remove nil cons cons 154 ref cons nil cons cons 162 ref subst eqMp eqMp 1054 def appThm sym nil 74 ref 629 remove cons 70 ref 631 remove cons nil cons cons nil cons cons 483 remove 477 remove nil 639 remove 91 ref 476 remove nil cons cons nil cons cons nil cons cons 152 ref subst 195 ref 474 remove 196 ref cons nil cons cons 162 ref subst eqMp eqMp nil 90 ref 268 remove nil cons cons 91 ref 482 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 172 ref 479 remove 199 ref cons nil cons cons 162 ref subst eqMp eqMp subst eqMp eqMp absThm eqMp eqMp nil 128 ref 364 remove cons 130 ref 362 remove cons nil cons cons nil cons cons 144 ref subst deductAntisym eqMp eqMp absThm eqMp nil 260 ref 1050 remove appTerm thm nil "P" 0 ref 0 ref 0 ref 2 ref 0 ref 3 ref "C" varType 1055 def nil cons 1056 def cons 1057 def opType 1058 def nil cons 1059 def cons opType 1060 def 8 ref cons opType 1061 def 8 ref cons opType 1062 def var 1063 def "p" 1061 ref var 1064 def 39 ref 40 ref 1062 ref constTerm 1065 def "f" 1060 ref var 1066 def 1064 ref varTerm 1067 def 1066 ref varTerm 1068 def appTerm 1069 def absTerm 1070 def appTerm 1071 def appTerm 1072 def 40 ref 0 ref 0 ref 0 ref 6 ref 1056 ref cons opType 1073 def 8 ref cons opType 1074 def 8 ref cons opType 1075 def constTerm 1076 def "f" 1073 ref var 1077 def 1067 ref 70 ref 74 ref 1077 ref varTerm 1078 def 79 ref appTerm 1079 def absTerm absTerm 1080 def appTerm 1081 def absTerm 1082 def appTerm 1083 def appTerm 1084 def absTerm 1085 def nil cons cons nil cons nil cons cons "A" 1061 ref nil cons cons nil cons 35 ref cons 59 ref subst 1086 def subst 1064 ref nil 61 ref 1084 remove nil cons cons nil cons nil cons cons 67 ref subst nil 90 ref 1071 ref nil cons 1087 def cons 1088 def 91 ref 1083 ref nil cons 1089 def cons 1090 def nil cons cons nil cons cons 986 ref subst nil 1088 ref 91 ref 39 ref 1083 ref appTerm 1091 def 50 ref appTerm 1092 def nil cons 1093 def cons nil cons cons nil cons cons 1094 def 109 ref subst 1094 remove 160 ref subst 1076 ref refl 1095 def 1077 ref nil 1066 ref 1080 ref nil cons cons nil cons nil cons cons nil 61 ref 1069 ref nil cons 1096 def cons nil cons nil cons cons 1097 def 67 ref subst 1098 def 1070 ref 1068 ref appTerm 1099 def betaConv nil 1088 ref 91 ref 1099 remove nil cons cons nil cons cons nil cons cons 152 ref subst "A" 1060 ref nil cons cons nil cons 1100 def "P" 1061 remove var 1101 def 1070 ref nil cons cons 1102 def "x" 1060 ref var 1068 ref nil cons 1103 def cons nil cons 1104 def cons nil cons cons 162 ref subst eqMp eqMp eqMp subst absThm appThm 705 ref "A" 1073 ref nil cons 1105 def cons nil cons 1106 def 35 ref cons 1107 def 61 ref 39 ref 43 ref 49 ref 63 ref absTerm appTerm appTerm 63 ref appTerm absTerm 1108 def 63 ref appTerm 1109 def betaConv nil 230 ref 1108 ref appTerm 1110 def axiom nil 90 ref 1110 remove nil cons cons 91 ref 1109 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 251 ref 252 ref 1108 remove nil cons cons 284 ref cons nil cons cons 162 ref subst eqMp eqMp 1111 def subst subst 1112 def trans eqMp nil 128 ref 1087 ref cons 130 ref 1093 remove cons nil cons cons nil cons cons 144 ref subst deductAntisym eqMp nil 90 ref 92 ref 1071 ref appTerm 1113 def 1092 remove appTerm nil cons cons 91 ref 39 ref 1113 ref 1083 ref appTerm 1114 def appTerm 1115 def 1113 ref 50 ref appTerm appTerm nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp nil "q'" 7 ref var 1116 def 704 remove cons nil cons nil cons cons 1117 def 1071 ref refl nil 90 ref 1072 ref 1071 ref appTerm nil cons cons 91 ref 92 ref 1113 ref 1091 remove 1116 ref varTerm 1118 def appTerm 1119 def appTerm appTerm 1115 ref 1113 remove 1118 ref appTerm appTerm appTerm nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp nil "p'" 7 ref var 1120 def 1087 ref cons nil cons nil cons cons 1116 ref 92 ref 1072 remove 1120 ref varTerm 1121 def appTerm appTerm 92 ref 92 ref 1121 ref appTerm 1122 def 1119 remove appTerm appTerm 1115 remove 1122 ref 1118 ref appTerm 1123 def appTerm appTerm appTerm absTerm 1124 def 1118 ref appTerm 1125 def betaConv 1120 ref 230 ref 1124 ref appTerm 1126 def absTerm 1127 def 1121 ref appTerm 1128 def betaConv nil 1090 remove 1088 remove nil cons cons nil cons cons nil 252 ref 1120 ref 230 ref 1116 ref 92 ref 239 remove 1121 ref appTerm 1129 def appTerm 92 ref 1122 ref 39 ref 95 ref appTerm 1118 ref appTerm 1130 def appTerm 1131 def appTerm 97 remove 1123 ref appTerm 1132 def appTerm 1133 def appTerm 1134 def absTerm 1135 def appTerm 1136 def absTerm nil cons cons nil cons nil cons cons 292 ref 59 ref subst 1137 def subst 1120 ref nil 61 ref 1136 remove nil cons cons nil cons nil cons cons 67 ref subst nil 252 ref 1135 remove nil cons cons nil cons nil cons cons 1137 ref subst 1116 ref nil 61 ref 1134 remove nil cons cons nil cons nil cons cons 67 ref subst nil 90 ref 1129 remove nil cons 1138 def cons 1139 def 91 ref 1133 remove nil cons 1140 def cons nil cons cons nil cons cons 1141 def 109 ref subst 1141 remove 160 ref subst nil 90 ref 1131 ref nil cons 1142 def cons 91 ref 1132 remove nil cons 1143 def cons nil cons cons nil cons cons 1144 def 109 ref subst 1144 remove 160 ref subst nil 975 ref 91 ref 1123 ref nil cons 1145 def cons nil cons cons nil cons cons 1146 def 986 ref subst 1146 ref 109 ref subst 1146 remove 160 ref subst nil 90 ref 1121 ref nil cons 1147 def cons 1148 def 91 ref 1118 ref nil cons 1149 def cons nil cons 1150 def cons nil cons cons 1151 def 109 ref subst 1151 ref 160 ref subst nil 1139 ref 91 ref 94 remove 1121 ref appTerm 1152 def nil cons 1153 def cons nil cons cons nil cons cons 152 ref subst nil 90 ref 121 remove cons 1154 def 91 ref 1147 ref cons nil cons cons nil cons cons 1155 def 250 ref subst eqMp 1156 def nil 90 ref 1153 ref cons 1157 def 1150 ref cons nil cons cons 1158 def 152 ref subst proveHyp nil 1139 remove 91 ref 1122 ref 93 ref appTerm 1159 def nil cons 1160 def cons nil cons cons nil cons cons 152 ref subst 1155 ref nil 242 remove 977 remove cons nil cons cons 1161 def 109 ref subst 1161 remove 160 ref subst 981 remove eqMp nil 248 remove 984 remove cons nil cons cons 144 ref subst deductAntisym eqMp 1162 def subst eqMp 1163 def nil 90 ref 1160 ref cons 1164 def 91 ref 92 ref 1152 ref appTerm 1165 def 1118 ref appTerm nil cons 1166 def cons nil cons cons nil cons cons 1167 def 152 ref subst proveHyp 1167 ref 109 ref subst 1167 remove 160 ref subst 1158 ref 109 ref subst 1158 remove 160 ref subst nil 1148 ref 982 remove cons nil cons cons 152 ref subst 1159 remove assume eqMp 1168 def 1155 remove 152 ref subst 1152 remove assume eqMp 1169 def 1168 remove proveHyp proveHyp nil 1148 remove 91 ref 1130 remove nil cons 1170 def cons nil cons cons nil cons cons 152 ref subst 1131 remove assume eqMp 1171 def nil 90 ref 1170 remove cons 1172 def 91 ref 463 remove 1118 ref appTerm 1173 def nil cons 1174 def cons nil cons cons nil cons cons 152 ref subst proveHyp nil 978 ref 1150 ref cons nil cons cons 1175 def 250 remove subst eqMp 1176 def nil 90 ref 1174 ref cons 1177 def 1150 remove cons nil cons cons 1178 def 152 ref subst proveHyp 1171 remove nil 1172 remove 91 ref 92 ref 1118 ref appTerm 95 ref appTerm 1179 def nil cons 1180 def cons nil cons cons nil cons cons 152 ref subst proveHyp 1175 ref 1162 remove subst eqMp 1181 def nil 90 ref 1180 ref cons 1182 def 91 ref 92 ref 1173 ref appTerm 1183 def 1118 ref appTerm nil cons 1184 def cons nil cons cons nil cons cons 1185 def 152 ref subst proveHyp 1185 ref 109 ref subst 1185 remove 160 ref subst 1178 ref 109 ref subst 1178 remove 160 ref subst 151 ref 1175 remove 152 ref subst 1173 remove assume eqMp proveHyp eqMp nil 128 ref 1174 remove cons 1186 def 130 ref 1149 ref cons nil cons 1187 def cons nil cons cons 144 ref subst deductAntisym eqMp eqMp nil 128 ref 1180 remove cons 1188 def 130 ref 1184 remove cons nil cons cons nil cons cons 144 ref subst deductAntisym eqMp eqMp eqMp proveHyp eqMp nil 128 ref 1153 remove cons 1189 def 1187 ref cons nil cons cons 144 ref subst deductAntisym eqMp eqMp nil 128 ref 1160 remove cons 1190 def 130 ref 1166 remove cons nil cons cons nil cons cons 144 ref subst deductAntisym eqMp eqMp eqMp eqMp nil 128 ref 1147 ref cons 1187 remove cons nil cons cons 144 ref subst deductAntisym eqMp eqMp nil 983 ref 130 ref 1145 ref cons nil cons cons nil cons cons 144 ref subst deductAntisym eqMp nil 90 ref 92 ref 96 ref appTerm 1123 ref appTerm nil cons cons 91 ref 92 ref 1123 ref appTerm 96 remove appTerm nil cons cons nil cons cons nil cons cons 160 ref subst proveHyp nil 90 ref 1145 ref cons 244 remove cons nil cons cons 1191 def 109 ref subst 1191 remove 160 ref subst 109 ref 160 ref 1156 remove nil 1157 remove 979 ref cons nil cons cons 1192 def 152 ref subst proveHyp 1163 remove nil 1164 remove 91 ref 1165 remove 95 ref appTerm nil cons 1193 def cons nil cons cons nil cons cons 1194 def 152 ref subst proveHyp 1194 ref 109 ref subst 1194 remove 160 ref subst 1192 ref 109 ref subst 1192 remove 160 ref subst 1169 remove 1176 remove nil 1177 remove 979 ref cons nil cons cons 1195 def 152 ref subst proveHyp 1181 remove nil 1182 remove 91 ref 1183 remove 95 ref appTerm nil cons 1196 def cons nil cons cons nil cons cons 1197 def 152 ref subst proveHyp 1197 ref 109 ref subst 1197 remove 160 ref subst 1195 ref 109 ref subst 1195 remove 160 ref subst 1151 remove 152 ref subst 1123 ref assume eqMp nil 90 ref 1149 ref cons 979 remove cons nil cons cons 152 ref subst 1179 remove assume eqMp proveHyp eqMp nil 1186 remove 131 ref cons nil cons cons 144 ref subst deductAntisym eqMp eqMp nil 1188 remove 130 ref 1196 remove cons nil cons cons nil cons cons 144 ref subst deductAntisym eqMp eqMp eqMp proveHyp eqMp nil 1189 remove 131 remove cons nil cons cons 144 ref subst deductAntisym eqMp eqMp nil 1190 remove 130 ref 1193 remove cons nil cons cons nil cons cons 144 ref subst deductAntisym eqMp eqMp eqMp eqMp 145 remove deductAntisym eqMp eqMp nil 128 ref 1145 remove cons 249 remove cons nil cons cons 144 ref subst deductAntisym eqMp eqMp eqMp eqMp nil 128 ref 1142 remove cons 130 ref 1143 remove cons nil cons cons nil cons cons 144 ref subst deductAntisym eqMp eqMp nil 128 ref 1138 remove cons 130 ref 1140 remove cons nil cons cons nil cons cons 144 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp absThm eqMp 1198 def subst nil 90 ref 230 ref 1127 ref appTerm nil cons cons 91 ref 1128 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 251 ref 252 ref 1127 remove nil cons cons 253 ref 1147 remove cons nil cons 1199 def cons nil cons cons 162 ref subst eqMp eqMp nil 90 ref 1126 remove nil cons cons 91 ref 1125 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 251 ref 252 ref 1124 remove nil cons cons 253 ref 1149 remove cons nil cons 1200 def cons nil cons cons 162 ref subst eqMp eqMp subst eqMp subst eqMp nil 61 ref 1087 ref cons nil cons nil cons cons 702 ref subst trans sym 66 ref eqMp nil 90 ref 1114 remove nil cons cons 91 ref 92 ref 1083 remove appTerm 1071 remove appTerm nil cons cons nil cons cons nil cons cons 160 ref subst proveHyp nil 90 ref 1089 ref cons 1201 def 91 ref 1087 ref cons nil cons cons nil cons cons 1202 def 109 ref subst 1202 remove 160 ref subst nil 1102 remove nil cons nil cons cons 1100 ref 35 ref cons 1203 def 59 ref subst 1204 def subst 1066 ref 1098 ref 1082 ref "select" const 1205 def 0 ref 1074 ref 1105 remove cons opType constTerm 1206 def 1077 ref 43 ref 70 ref 189 ref 74 ref 12 ref 0 ref 1055 ref 0 ref 1055 ref 8 ref cons opType 1207 def nil cons 1208 def cons opType constTerm 1209 def 1079 ref appTerm 1068 ref 76 ref appTerm 1210 def 78 ref appTerm 1211 def appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1212 def appTerm 1213 def betaConv nil 1201 remove 91 ref 1213 remove nil cons cons nil cons cons nil cons cons 152 ref subst 1106 ref "P" 1074 ref var 1214 def 1082 ref nil cons 1215 def cons "x" 1073 ref var 1216 def 1212 ref nil cons cons nil cons cons nil cons cons 162 ref subst eqMp eqMp nil 90 ref 1067 ref 70 ref 74 ref 1212 ref 79 ref appTerm absTerm absTerm appTerm 1217 def nil cons cons 1218 def 91 ref 1096 ref cons 1219 def nil cons cons nil cons cons 152 ref subst proveHyp nil 90 ref 1096 ref cons 91 ref 39 ref 1069 ref appTerm 1220 def 50 ref appTerm 1221 def nil cons 1222 def cons nil cons cons nil cons cons 1223 def 109 ref subst 1223 remove 160 ref subst 1098 remove 1069 ref assume eqMp eqMp nil 128 ref 1096 ref cons 130 ref 1222 remove cons nil cons cons nil cons cons 144 ref subst deductAntisym eqMp nil 90 ref 92 ref 1069 ref appTerm 1224 def 1221 remove appTerm nil cons cons 91 ref 39 ref 92 ref 1217 ref appTerm 1069 ref appTerm appTerm 1225 def 1224 ref 50 ref appTerm appTerm nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 1117 ref 1067 remove refl 70 ref 74 ref 74 ref 1209 ref 1206 ref "_1480" 1073 ref var 1226 def 43 ref 70 ref 189 ref 74 ref 1209 ref 1226 remove varTerm 79 ref appTerm appTerm 1211 ref appTerm absTerm appTerm absTerm appTerm absTerm 1227 def appTerm 1228 def 79 ref appTerm appTerm 1211 ref appTerm absTerm 1229 def 78 ref appTerm 1230 def betaConv 70 ref 189 ref 1229 ref appTerm 1231 def absTerm 1232 def 76 ref appTerm 1233 def betaConv 1227 ref 1228 remove appTerm 1234 def betaConv "fn" 1073 ref var 1235 def 43 ref 70 ref 189 ref 74 ref 1209 ref 1235 ref varTerm 1236 def 79 ref appTerm appTerm 1237 def 1211 ref appTerm absTerm appTerm absTerm appTerm absTerm 1238 def 11 ref 1068 ref 23 ref appTerm 27 ref appTerm absTerm 1239 def appTerm betaConv sym 313 ref 70 ref 490 ref 74 ref 1209 ref refl 1240 def 1239 ref 79 ref appTerm betaConv 1241 def 1068 ref refl 200 ref appThm 209 ref appThm 1242 def trans appThm 1211 ref refl appThm nil "x" 1055 ref var 1243 def 1211 remove nil cons cons nil cons nil cons cons "A" 1056 ref cons 1244 def nil cons 1245 def 35 ref cons 1246 def 294 ref subst 1247 def subst trans absThm appThm 705 ref 173 ref 1111 ref subst subst 1248 def trans absThm appThm 705 ref 1111 ref subst 1249 def trans sym 66 ref eqMp eqMp 1106 ref 1214 ref 1238 ref nil cons cons 1216 ref 1239 ref nil cons cons nil cons cons nil cons cons 238 remove sym nil 252 ref 130 ref 92 ref 215 ref appTerm 1250 def 135 ref appTerm 1251 def absTerm nil cons cons nil cons nil cons cons 1137 remove subst 130 ref nil 61 ref 1251 remove nil cons cons nil cons nil cons cons 67 ref subst 227 ref 109 ref subst 227 remove 160 ref subst nil 90 ref 158 ref cons 225 ref cons nil cons cons 1252 def 152 ref subst 1253 def 214 ref 156 ref appTerm 1254 def betaConv nil 217 ref 91 ref 1254 remove nil cons cons nil cons cons nil cons cons 152 ref subst 195 ref 44 ref 214 remove nil cons cons 1255 def 49 ref 156 ref nil cons 1256 def cons nil cons 1257 def cons nil cons cons 162 ref subst eqMp eqMp 1258 def eqMp eqMp nil 255 ref 254 ref cons nil cons cons 144 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp 1259 def subst proveHyp 1260 def nil 90 ref 68 ref 1075 ref constTerm 1261 def 1227 ref appTerm nil cons cons 91 ref 1234 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp nil "p" 1074 ref var 1262 def 1227 remove nil cons cons nil cons nil cons cons 1107 ref nil 90 ref 69 ref 48 ref appTerm 1263 def nil cons 1264 def cons 1265 def 91 ref 39 ref 48 ref 1205 ref 0 ref 41 ref 19 ref cons opType constTerm 48 ref appTerm appTerm 1266 def appTerm 1267 def 50 ref appTerm 1268 def nil cons 1269 def cons nil cons 1270 def cons nil cons cons 1271 def 109 ref subst 1271 remove 160 ref subst 475 ref nil 314 remove 354 ref cons nil cons nil cons cons 318 remove 332 ref 323 remove appTerm 1272 def betaConv 334 remove nil 90 ref 333 remove nil cons cons 91 ref 1272 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 336 ref 337 ref 332 remove nil cons cons 339 remove cons nil cons cons 162 ref subst eqMp eqMp 1273 def subst subst appThm 1274 def nil 61 ref 1264 ref cons nil cons nil cons cons 1275 def 67 ref subst 1263 ref assume eqMp trans sym 66 ref eqMp nil 90 ref 510 ref nil cons cons 1276 def 1270 ref cons nil cons cons 152 ref subst proveHyp nil 44 ref 354 ref cons 130 ref 1269 remove cons nil cons 1277 def cons nil cons cons nil 217 remove 91 ref 92 ref 69 ref 49 ref 157 ref absTerm 1278 def appTerm 1279 def appTerm 135 ref appTerm 1280 def nil cons 1281 def cons nil cons 1282 def cons nil cons cons 1283 def 986 ref subst 1283 ref 109 ref subst 1283 remove 160 ref subst nil 44 ref 49 ref 92 ref 1278 ref 156 ref appTerm 1284 def appTerm 135 remove appTerm 1285 def absTerm 1286 def nil cons cons nil cons nil cons cons 59 ref subst 49 ref nil 61 ref 1285 remove nil cons cons nil cons nil cons cons 67 ref subst nil 90 ref 1284 ref nil cons 1287 def cons 225 ref cons nil cons cons 1288 def 109 ref subst 1288 remove 160 ref subst nil "f" 41 remove var 315 ref cons 954 ref 1256 ref cons nil cons cons nil cons cons 316 remove 195 ref cons 35 ref cons 954 ref 202 ref 49 ref "f" 319 ref var 1289 def varTerm 1290 def 156 ref appTerm 1291 def absTerm 955 ref appTerm appTerm 1290 ref 955 ref appTerm appTerm absTerm 1292 def 955 ref appTerm 1293 def betaConv 1289 ref 43 ref 1292 ref appTerm 1294 def absTerm 1295 def 1290 ref appTerm 1296 def betaConv nil 329 ref 1295 ref appTerm 1297 def axiom nil 90 ref 1297 remove nil cons cons 91 ref 1296 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 336 ref 337 ref 1295 remove nil cons cons 338 ref 1290 ref nil cons cons nil cons 1298 def cons nil cons cons 162 ref subst eqMp eqMp nil 90 ref 1294 remove nil cons cons 91 ref 1293 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 195 ref 44 ref 1292 remove nil cons cons 995 ref cons nil cons cons 162 ref subst eqMp eqMp 1299 def subst subst 1300 def 1284 remove assume eqMp 1253 remove proveHyp 1258 remove eqMp eqMp nil 128 ref 1287 remove cons 254 ref cons nil cons cons 144 ref subst deductAntisym eqMp eqMp absThm eqMp nil 90 ref 43 ref 1286 remove appTerm nil cons cons 1282 remove cons nil cons cons 152 ref subst proveHyp 195 ref 44 ref 1278 remove nil cons cons 1301 def 254 ref cons nil cons cons 256 ref subst eqMp eqMp nil 255 remove 130 ref 1281 ref cons nil cons cons nil cons cons 144 ref subst deductAntisym eqMp nil 90 ref 1250 remove 1280 ref appTerm nil cons cons 91 ref 92 ref 1280 ref appTerm 215 remove appTerm nil cons cons nil cons cons nil cons cons 160 ref subst proveHyp nil 90 ref 1281 ref cons 91 ref 216 ref cons nil cons cons nil cons cons 1302 def 109 ref subst 1302 remove 160 ref subst nil 1255 remove nil cons nil cons cons 59 ref subst 49 ref nil 61 ref 213 remove nil cons cons nil cons nil cons cons 67 ref subst 1252 ref 109 ref subst 1252 remove 160 ref subst 1300 remove sym 157 remove assume eqMp 195 ref 1301 remove 1257 ref cons nil cons cons 1259 ref subst proveHyp nil 90 ref 1279 remove nil cons cons 225 remove cons nil cons cons 152 ref subst 1280 remove assume eqMp proveHyp eqMp nil 128 ref 158 remove cons 254 remove cons nil cons cons 144 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp nil 128 ref 1281 remove cons 130 ref 216 remove cons nil cons cons nil cons cons 144 ref subst deductAntisym eqMp eqMp eqMp subst nil 44 ref 49 ref 236 ref 1268 ref appTerm 1303 def absTerm nil cons cons nil cons nil cons cons 59 ref subst 49 ref nil 61 ref 1303 remove nil cons cons nil cons nil cons cons 67 ref subst nil 90 ref 235 ref nil cons 1304 def cons 1305 def 1270 remove cons nil cons cons 1306 def 109 ref subst 1306 remove 160 ref subst nil 61 ref 1266 ref nil cons 1307 def cons nil cons nil cons cons 67 ref subst nil 1305 ref 91 ref 1307 remove cons 1308 def nil cons cons nil cons cons 152 ref subst 49 ref 236 remove 1266 ref appTerm absTerm 1309 def 156 ref appTerm 1310 def betaConv 47 ref 43 ref 1309 ref appTerm 1311 def absTerm 1312 def 48 ref appTerm 1313 def betaConv nil 349 ref 1312 ref appTerm 1314 def axiom 1315 def nil 90 ref 1314 remove nil cons cons 1316 def 91 ref 1313 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 351 ref 352 ref 1312 ref nil cons cons 1317 def 355 ref cons nil cons cons 162 ref subst eqMp eqMp nil 90 ref 1311 remove nil cons cons 91 ref 1310 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 195 ref 44 ref 1309 remove nil cons cons 1257 ref cons nil cons cons 162 ref subst eqMp eqMp eqMp eqMp eqMp nil 128 ref 1304 ref cons 1318 def 1277 ref cons nil cons cons 144 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp eqMp eqMp nil 128 ref 1264 ref cons 1277 remove cons nil cons cons 144 ref subst deductAntisym eqMp nil 90 ref 92 ref 1263 ref appTerm 1319 def 1268 remove appTerm nil cons cons 91 ref 39 ref 1319 ref 1266 remove appTerm appTerm 1320 def 1319 ref 50 ref appTerm appTerm nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 1117 remove 1263 ref refl nil 90 ref 39 ref 1263 ref appTerm 1321 def 1263 ref appTerm nil cons cons 91 ref 92 ref 1319 ref 1267 remove 1118 ref appTerm 1322 def appTerm appTerm 1320 ref 1319 remove 1118 ref appTerm appTerm appTerm nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp nil 1120 ref 1264 remove cons nil cons nil cons cons 1116 ref 92 ref 1321 remove 1121 ref appTerm appTerm 92 ref 1122 ref 1322 remove appTerm appTerm 1320 remove 1123 ref appTerm appTerm appTerm absTerm 1323 def 1118 ref appTerm 1324 def betaConv 1120 ref 230 ref 1323 ref appTerm 1325 def absTerm 1326 def 1121 ref appTerm 1327 def betaConv nil 1308 remove 1265 remove nil cons cons nil cons cons 1198 ref subst nil 90 ref 230 ref 1326 ref appTerm nil cons cons 91 ref 1327 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 251 ref 252 ref 1326 remove nil cons cons 1199 ref cons nil cons cons 162 ref subst eqMp eqMp nil 90 ref 1325 remove nil cons cons 91 ref 1324 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 251 ref 252 ref 1323 remove nil cons cons 1200 ref cons nil cons cons 162 ref subst eqMp eqMp subst eqMp subst eqMp 1275 remove 702 ref subst trans sym 66 ref eqMp 1328 def subst 1329 def subst eqMp eqMp nil 90 ref 43 ref 1232 ref appTerm nil cons cons 91 ref 1233 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 195 ref 44 ref 1232 remove nil cons cons 196 ref cons nil cons cons 162 ref subst eqMp eqMp nil 90 ref 1231 remove nil cons cons 91 ref 1230 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 172 ref 168 ref 1229 remove nil cons cons 199 ref cons nil cons cons 162 ref subst eqMp eqMp absThm nil "t" 1058 ref var 1210 remove nil cons cons nil cons nil cons cons 171 ref "B" 1056 ref cons 1330 def nil cons 1331 def cons 35 ref cons 1332 def 1273 ref subst subst trans absThm nil "t" 1060 ref var 1103 remove cons nil cons nil cons cons 194 ref "B" 1059 remove cons nil cons cons 35 ref cons 1273 ref subst subst trans appThm nil 90 ref 39 ref 1217 remove appTerm 1333 def 1069 ref appTerm nil cons cons 91 ref 92 ref 1224 ref 1220 remove 1118 ref appTerm 1334 def appTerm appTerm 1225 ref 1224 remove 1118 ref appTerm appTerm appTerm nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp nil 1120 ref 1096 remove cons nil cons nil cons cons 1116 remove 92 ref 1333 remove 1121 ref appTerm appTerm 92 ref 1122 remove 1334 remove appTerm appTerm 1225 remove 1123 remove appTerm appTerm appTerm absTerm 1335 def 1118 remove appTerm 1336 def betaConv 1120 remove 230 ref 1335 ref appTerm 1337 def absTerm 1338 def 1121 remove appTerm 1339 def betaConv nil 1219 remove 1218 remove nil cons cons nil cons cons 1198 remove subst nil 90 ref 230 ref 1338 ref appTerm nil cons cons 91 ref 1339 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 251 ref 252 ref 1338 remove nil cons cons 1199 remove cons nil cons cons 162 ref subst eqMp eqMp nil 90 ref 1337 remove nil cons cons 91 ref 1336 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 251 ref 252 ref 1335 remove nil cons cons 1200 remove cons nil cons cons 162 ref subst eqMp eqMp subst eqMp subst eqMp 1097 remove 702 remove subst trans sym 66 ref eqMp eqMp eqMp absThm eqMp eqMp nil 128 ref 1089 remove cons 130 ref 1087 remove cons nil cons cons nil cons cons 144 ref subst deductAntisym eqMp eqMp eqMp 1340 def eqMp absThm eqMp nil 40 ref 0 ref 1062 ref 8 ref cons opType constTerm 1341 def 1085 remove appTerm thm nil 1063 remove 1064 ref 39 ref 68 ref 1062 remove constTerm 1342 def 1070 remove appTerm 1343 def appTerm 1261 ref 1082 ref appTerm 1344 def appTerm 1345 def absTerm 1346 def nil cons cons nil cons nil cons cons 1086 remove subst 1064 ref nil 61 ref 1345 remove nil cons 1347 def cons nil cons nil cons cons 67 ref subst 132 ref 1203 ref 866 ref subst 132 ref 1065 ref refl 1348 def 1066 ref 1066 ref 275 ref 1069 remove appTerm absTerm 1349 def 1068 ref appTerm betaConv absThm appThm appThm 1095 ref 1077 ref 1349 ref 1080 ref appTerm betaConv absThm appThm appThm nil 1064 ref 1349 remove nil cons cons nil cons nil cons cons 1340 ref subst eqMp trans appThm 132 ref 312 ref 1261 ref refl 1350 def 1077 ref 1082 remove 1078 ref appTerm betaConv 1351 def absThm appThm appThm appThm 1095 ref 1077 ref 312 ref 1351 remove appThm absThm appThm appThm nil 1262 ref 1215 remove cons nil cons nil cons cons 1107 ref 866 ref subst subst eqMp appThm nil 253 ref 1076 ref 1077 ref 275 ref 1081 remove appTerm absTerm appTerm nil cons cons nil cons nil cons cons 295 ref subst trans sym 66 ref eqMp nil 90 ref 39 ref 275 ref 1343 ref appTerm appTerm 275 ref 1344 ref appTerm appTerm nil cons cons 91 ref 1347 remove cons nil cons cons nil cons cons 152 ref subst proveHyp nil "y" 7 ref var 1352 def 1344 remove nil cons cons 253 ref 1343 remove nil cons cons nil cons cons nil cons cons nil 90 ref 39 ref 253 ref varTerm 1353 def appTerm 1354 def 279 ref appTerm 1355 def nil cons 1356 def cons 91 ref 92 ref 39 ref 275 ref 1353 ref appTerm appTerm 275 ref 1352 ref varTerm 1357 def appTerm 1358 def appTerm appTerm 1354 ref 1357 ref appTerm appTerm nil cons 1359 def cons nil cons 1360 def cons nil cons cons 1361 def 109 ref subst 1361 remove 160 ref subst 39 ref "_1484" 7 ref var 1362 def 92 ref 39 ref 275 ref 1362 remove varTerm 1363 def appTerm appTerm 1358 ref appTerm appTerm 39 ref 1363 remove appTerm 1357 ref appTerm appTerm absTerm 1364 def 1353 ref appTerm 1365 def appTerm refl 1366 def 1364 ref 279 ref appTerm betaConv appThm 132 ref 1365 remove betaConv appThm 1367 def 92 ref 401 ref 1358 ref appTerm appTerm 380 remove 1357 ref appTerm appTerm refl appThm trans 1364 remove refl 1368 def 1355 remove assume appThm eqMp sym 713 ref 132 ref 402 remove appThm 1369 def 1358 ref refl 1370 def appThm nil 61 ref 1358 ref nil cons cons nil cons nil cons cons 1371 def 431 ref subst trans appThm nil 61 ref 1357 ref nil cons cons nil cons nil cons cons 1372 def 390 ref subst appThm 1371 ref 827 ref subst trans sym 66 ref eqMp eqMp eqMp nil 128 ref 1356 ref cons 130 ref 1359 ref cons nil cons 1373 def cons nil cons cons 144 ref subst deductAntisym eqMp nil 90 ref 1354 remove 50 ref appTerm 1374 def nil cons 1375 def cons 1360 remove cons nil cons cons 1376 def 109 ref subst 1376 remove 160 ref subst 1366 remove "_1482" 7 ref var 1377 def 92 ref 39 ref 275 ref 1377 remove varTerm 1378 def appTerm appTerm 1358 ref appTerm appTerm 39 ref 1378 remove appTerm 1357 ref appTerm appTerm absTerm 50 ref appTerm betaConv appThm 1367 remove 92 ref 433 ref 1358 remove appTerm appTerm 423 remove 1357 remove appTerm appTerm refl appThm trans 1368 remove 1374 remove assume appThm eqMp sym 713 ref 132 ref 434 remove appThm 1379 def 1370 remove appThm 1371 remove 390 ref subst 1372 ref 289 ref subst trans trans appThm 1372 ref 431 ref subst appThm 1372 remove 827 ref subst trans sym 66 ref eqMp eqMp eqMp nil 128 ref 1375 remove cons 1380 def 1373 remove cons nil cons cons 144 ref subst deductAntisym eqMp 442 remove 1353 ref appTerm 1381 def betaConv 445 remove nil 446 remove 91 ref 1381 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 251 ref 447 remove 253 ref 1353 remove nil cons cons nil cons cons nil cons cons 162 ref subst eqMp eqMp nil 1380 remove 130 ref 1356 remove cons 450 ref 1359 remove cons nil cons cons cons nil cons cons 469 ref subst proveHyp proveHyp proveHyp subst eqMp 1382 def eqMp absThm eqMp nil 1341 remove 1346 remove appTerm thm nil 1101 ref 1066 ref 1261 ref 1238 remove appTerm 1383 def absTerm 1384 def nil cons cons nil cons nil cons cons 1204 remove subst 1066 ref nil 61 ref 1383 remove nil cons cons nil cons nil cons cons 67 ref subst 1260 ref eqMp absThm eqMp nil 1065 ref 1384 remove appTerm thm 40 ref 0 ref 0 ref 0 ref 2 ref 201 remove cons opType 1385 def 8 ref cons opType 1386 def 8 ref cons opType constTerm 1387 def refl 1388 def "p" 1385 ref var 1389 def 39 ref 43 ref 49 ref 189 ref "y" 3 ref var 1390 def 1389 ref varTerm 1391 def 156 ref appTerm 1392 def 1390 ref varTerm 1393 def appTerm absTerm 1394 def appTerm absTerm appTerm 1395 def appTerm 1396 def refl 132 ref 471 ref 940 ref 940 remove 1391 ref 21 ref 946 ref appTerm appTerm 26 ref 946 ref appTerm appTerm absTerm 1397 def 946 remove appTerm betaConv absThm 1398 def appThm appThm 313 ref 70 ref 490 ref 74 ref 1397 ref 79 ref appTerm betaConv absThm 1399 def appThm absThm appThm appThm nil 261 ref 1397 ref nil cons cons nil cons nil cons cons 1400 def 361 remove 847 remove nil 273 remove 91 ref 360 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 310 ref 309 remove 844 ref 262 ref nil cons cons nil cons 1401 def cons nil cons cons 162 ref subst eqMp eqMp 1402 def subst eqMp 313 ref 70 ref 490 ref 74 ref 1391 ref refl 1403 def 200 ref appThm 209 ref appThm absThm 1404 def appThm absThm appThm trans appThm nil 253 ref 1395 remove nil cons cons nil cons nil cons cons 295 ref subst trans absThm appThm 705 ref "A" 1385 ref nil cons cons nil cons 1405 def 35 ref cons 1406 def 1111 ref subst subst 1407 def trans sym 66 ref eqMp nil 1387 ref 1389 ref 1396 remove 88 ref 1397 ref appTerm appTerm absTerm appTerm thm 1388 ref 1389 ref 39 ref 69 ref 49 ref 73 ref 1394 remove appTerm absTerm appTerm 1408 def appTerm 1409 def refl 132 ref 488 remove 1398 remove appThm appThm 475 ref 70 ref 481 ref 1399 remove appThm absThm appThm appThm 1400 remove 859 remove 1048 remove nil 853 remove 91 ref 858 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 310 ref 857 remove 1401 remove cons nil cons cons 162 ref subst eqMp eqMp subst eqMp 475 ref 70 ref 481 remove 1404 remove appThm absThm appThm trans 1410 def appThm nil 253 ref 1408 remove nil cons cons nil cons nil cons cons 295 ref subst trans absThm appThm 1407 ref trans sym 66 ref eqMp nil 1387 ref 1389 ref 1409 remove 487 ref 1397 remove appTerm appTerm absTerm appTerm thm nil "P" 0 ref 0 ref 0 ref 2 ref 1 ref 1057 remove opType 1411 def nil cons 1412 def cons 1413 def opType 1414 def 8 ref cons opType 1415 def 8 ref cons opType 1416 def var 1417 def "p" 1415 ref var 1418 def 39 ref 40 ref 1416 ref constTerm 1419 def "f" 1414 ref var 1420 def 1418 ref varTerm 1421 def 1420 ref varTerm 1422 def appTerm 1423 def absTerm 1424 def appTerm 1425 def appTerm 329 ref "g" 319 ref var 1426 def 40 ref 0 ref 0 ref 0 ref 2 ref 1056 ref cons opType 1427 def 8 ref cons opType 1428 def 8 ref cons opType 1429 def constTerm 1430 def "h" 1427 ref var 1431 def 1421 ref 70 ref 15 ref 0 ref 3 ref 0 ref 1055 ref 1412 ref cons opType nil cons cons opType constTerm 1432 def 1426 ref varTerm 1433 def 76 ref appTerm appTerm 1431 ref varTerm 1434 def 76 ref appTerm appTerm absTerm 1435 def appTerm 1436 def absTerm 1437 def appTerm 1438 def absTerm 1439 def appTerm 1440 def appTerm 1441 def absTerm 1442 def nil cons cons nil cons nil cons cons "A" 1415 ref nil cons cons nil cons 1443 def 35 ref cons 1444 def 59 ref subst subst 1418 ref nil 61 ref 1441 remove nil cons cons nil cons nil cons cons 67 ref subst nil 90 ref 1425 ref nil cons 1445 def cons 1446 def 91 ref 1440 ref nil cons 1447 def cons nil cons cons nil cons cons 1448 def 986 remove subst 1448 ref 109 ref subst 1448 remove 160 ref subst 330 ref 1426 ref 1430 ref refl 1449 def 1431 ref nil 1420 ref 1435 ref nil cons 1450 def cons nil cons nil cons cons nil 61 ref 1423 ref nil cons cons nil cons nil cons cons 67 ref subst 1451 def 1424 ref 1422 ref appTerm 1452 def betaConv nil 1446 remove 91 ref 1452 remove nil cons cons nil cons cons nil cons cons 152 ref subst "A" 1414 ref nil cons cons nil cons 1453 def "P" 1415 ref var 1424 ref nil cons cons 1454 def "x" 1414 ref var 1422 ref nil cons 1455 def cons nil cons cons nil cons cons 162 ref subst eqMp eqMp eqMp subst absThm appThm 705 ref "A" 1427 ref nil cons 1456 def cons 1457 def nil cons 1458 def 35 ref cons 1459 def 1111 ref subst subst trans absThm appThm 705 ref 336 ref 35 ref cons 1460 def 1111 ref subst subst trans sym 66 ref eqMp eqMp nil 128 ref 1445 ref cons 130 ref 1447 ref cons nil cons cons nil cons cons 144 ref subst deductAntisym eqMp nil 90 ref 92 ref 1425 ref appTerm 1440 ref appTerm nil cons cons 91 ref 92 ref 1440 remove appTerm 1425 remove appTerm nil cons cons nil cons cons nil cons cons 160 ref subst proveHyp nil 90 ref 1447 ref cons 1461 def 91 ref 1445 ref cons nil cons cons nil cons cons 1462 def 109 ref subst 1462 remove 160 ref subst nil 1454 remove nil cons nil cons cons 1453 remove 35 ref cons 1463 def 59 ref subst subst 1420 ref 1451 remove 1421 ref refl 1464 def nil "t" 1414 ref var 1455 remove cons nil cons nil cons cons 194 ref "B" 1412 ref cons 1465 def nil cons cons 35 ref cons 1466 def 340 remove subst subst appThm sym 1464 ref 49 ref nil "x" 1411 ref var 1422 ref 156 ref appTerm 1467 def nil cons cons nil cons nil cons cons 1332 ref 1054 ref subst subst absThm appThm sym 132 ref 1464 remove 49 ref 1432 ref refl 49 ref 18 ref 0 ref 1411 ref 4 ref cons opType 1468 def constTerm 1469 def 1467 ref appTerm absTerm 1470 def 156 ref appTerm betaConv appThm 49 ref 24 ref 0 ref 1411 ref 1056 ref cons opType 1471 def constTerm 1472 def 1467 remove appTerm absTerm 1473 def 156 ref appTerm betaConv appThm absThm appThm appThm 139 remove appThm nil 1426 ref 1470 remove nil cons cons 1431 ref 1473 remove nil cons cons nil cons cons nil cons cons nil 61 ref 1436 ref nil cons cons nil cons nil cons cons 67 ref subst 1437 ref 1434 ref appTerm 1474 def betaConv 1475 def 1439 ref 1433 ref appTerm 1476 def betaConv nil 1461 remove 91 ref 1476 remove nil cons cons nil cons cons nil cons cons 152 ref subst 336 ref 337 ref 1439 remove nil cons cons 338 remove 1433 ref nil cons 1477 def cons nil cons 1478 def cons nil cons cons 162 ref subst eqMp eqMp nil 90 ref 1438 remove nil cons cons 91 ref 1474 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 1458 remove "P" 1428 ref var 1437 ref nil cons 1479 def cons "x" 1427 ref var 1434 ref nil cons 1480 def cons nil cons cons nil cons cons 162 ref subst eqMp eqMp eqMp subst eqMp sym 66 ref eqMp eqMp eqMp eqMp absThm eqMp eqMp nil 128 ref 1447 remove cons 130 ref 1445 remove cons nil cons cons nil cons cons 144 ref subst deductAntisym eqMp eqMp eqMp 1481 def eqMp absThm eqMp nil 40 ref 0 ref 1416 ref 8 ref cons opType constTerm 1482 def 1442 remove appTerm thm 1482 ref refl 1483 def 1418 ref 132 ref 1463 remove nil 90 ref 39 ref 510 remove appTerm 275 ref 861 ref appTerm 1484 def appTerm 1485 def nil cons cons nil cons nil cons cons 296 ref subst sym nil 90 ref 275 ref 1485 remove appTerm 1486 def nil cons 1487 def cons 300 ref cons nil cons cons 1488 def 109 ref subst 1488 remove 160 ref subst nil 1276 remove 91 ref 1484 remove nil cons cons nil cons cons nil cons cons 470 remove subst 393 ref 400 ref 475 ref 49 ref 235 ref refl absThm appThm appThm nil 90 ref 861 ref nil cons 1489 def cons 1490 def nil cons 1491 def nil cons cons 290 ref subst appThm appThm 400 remove 866 remove appThm nil 44 ref 346 ref nil cons cons 1492 def nil cons nil cons cons 356 remove subst 475 ref 49 ref 312 ref 346 ref 156 ref appTerm betaConv appThm nil 1305 ref nil cons nil cons cons 290 remove subst trans absThm appThm trans appThm appThm trans 393 ref nil 91 ref 1489 ref cons nil cons nil cons cons 543 remove subst appThm nil 505 ref 354 remove cons 1491 remove cons nil cons cons 530 remove subst appThm 132 ref 393 ref 475 ref 49 ref 49 ref 536 remove 861 ref appTerm 1493 def absTerm 1494 def 156 ref appTerm betaConv 1495 def absThm appThm appThm 475 ref 49 ref 49 ref 98 ref 861 ref appTerm 235 remove appTerm 1496 def absTerm 1497 def 156 ref appTerm betaConv 1498 def absThm appThm appThm appThm 475 remove 49 ref 393 remove 1495 remove appThm 1498 remove appThm absThm appThm appThm nil 47 ref 1494 remove nil cons cons 505 remove 1497 remove nil cons cons nil cons cons nil cons cons 561 remove subst eqMp trans trans 1486 remove assume eqMp nil 90 ref 69 ref 49 ref 369 remove 1493 ref appTerm 1496 ref appTerm 1499 def absTerm 1500 def appTerm 1501 def nil cons cons 300 ref cons nil cons cons 152 ref subst proveHyp nil 44 ref 49 ref 92 ref 1500 ref 156 ref appTerm 1502 def appTerm 279 ref appTerm 1503 def absTerm 1504 def nil cons cons nil cons nil cons cons 59 ref subst 49 ref nil 61 ref 1503 remove nil cons cons nil cons nil cons cons 67 ref subst nil 90 ref 1502 ref nil cons 1505 def cons 300 ref cons nil cons cons 1506 def 109 ref subst 1506 remove 160 ref subst 1502 ref betaConv 1502 remove assume eqMp nil 90 ref 1499 remove nil cons 1507 def cons 300 ref cons nil cons cons 1508 def 152 ref subst proveHyp 1508 ref 109 ref subst 1508 remove 160 ref subst nil 90 ref 1496 remove nil cons 1509 def cons 300 ref cons nil cons cons 1510 def 109 ref subst 1510 remove 160 ref subst nil 128 ref 1489 ref cons 130 ref 1304 remove cons nil cons cons nil cons cons 1511 def 638 ref subst nil 1305 remove 300 ref cons nil cons cons 152 ref subst 1512 def proveHyp nil "_1495" 2 ref var 1513 def 1256 ref cons nil cons nil cons cons nil 90 ref 48 ref 1513 remove varTerm 1514 def appTerm nil cons cons nil cons nil cons cons 831 ref subst 346 ref 1514 ref appTerm 1515 def betaConv 1511 remove 144 ref subst nil 1490 ref 91 ref 1515 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 195 ref 1492 ref 49 ref 1514 remove nil cons cons nil cons cons nil cons cons 162 ref subst eqMp eqMp eqMp subst eqMp eqMp nil 128 ref 1509 ref cons 832 ref cons nil cons cons 144 ref subst deductAntisym eqMp nil 90 ref 1493 remove nil cons 1516 def cons 300 ref cons nil cons cons 1517 def 109 ref subst 1517 remove 160 ref subst nil 1318 remove 130 ref 1489 remove cons nil cons cons nil cons cons 1518 def 144 ref subst 1512 remove proveHyp nil "_1494" 2 ref var 1519 def 1256 ref cons nil cons nil cons cons nil 90 ref 48 ref 1519 remove varTerm 1520 def appTerm nil cons cons nil cons nil cons cons 831 ref subst 346 remove 1520 ref appTerm 1521 def betaConv 1518 remove 638 ref subst nil 1490 remove 91 ref 1521 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 195 ref 1492 remove 49 ref 1520 remove nil cons cons nil cons cons nil cons cons 162 ref subst eqMp eqMp eqMp subst eqMp eqMp nil 128 ref 1516 remove cons 1522 def 832 ref cons nil cons cons 144 ref subst deductAntisym eqMp nil 1522 remove 130 ref 1509 remove cons 843 remove cons cons nil cons cons 469 ref subst proveHyp proveHyp eqMp nil 128 ref 1507 remove cons 832 ref cons nil cons cons 144 ref subst deductAntisym eqMp eqMp eqMp nil 128 ref 1505 remove cons 832 ref cons nil cons cons 144 ref subst deductAntisym eqMp eqMp absThm eqMp nil 90 ref 43 ref 1504 remove appTerm nil cons cons 91 ref 92 ref 1501 remove appTerm 279 ref appTerm nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 195 ref 44 ref 1500 remove nil cons cons 832 ref cons nil cons cons 256 ref subst eqMp eqMp eqMp nil 128 ref 1487 remove cons 832 ref cons nil cons cons 144 ref subst deductAntisym eqMp eqMp 1523 def subst appThm 132 ref 68 ref 328 remove constTerm 1524 def refl 1525 def 1426 ref 1426 ref 68 ref 1429 remove constTerm 1526 def 1437 remove appTerm absTerm 1527 def 1433 ref appTerm betaConv 1528 def absThm appThm appThm 312 ref 330 ref 1426 ref 312 ref 1528 remove appThm absThm appThm appThm appThm nil "p" 321 remove var 1527 ref nil cons cons nil cons nil cons cons 1460 remove 1523 ref subst subst eqMp 312 ref 330 ref 1426 ref 312 ref 132 ref 1526 ref refl 1529 def 1431 ref 1475 ref absThm appThm appThm 312 ref 1449 ref 1431 ref 312 ref 1475 remove appThm absThm appThm appThm appThm nil "p" 1428 ref var 1479 remove cons nil cons nil cons cons 1459 remove 1523 remove subst subst eqMp appThm nil 61 ref 1430 ref 1431 ref 275 ref 1436 remove appTerm absTerm appTerm 1530 def nil cons cons nil cons nil cons cons 289 remove subst trans absThm appThm appThm trans appThm absThm appThm sym 1483 remove 1418 ref 132 ref 312 ref 132 ref 1419 ref refl 1531 def 1420 ref 1420 remove 275 ref 1423 remove appTerm absTerm 1532 def 1422 remove appTerm betaConv absThm appThm appThm 330 ref 1426 ref 1449 ref 1431 ref 1532 ref 1435 ref appTerm betaConv absThm appThm absThm appThm appThm nil 1418 ref 1532 remove nil cons cons nil cons nil cons cons 1481 ref subst eqMp appThm appThm 275 ref 329 ref 1426 ref 1530 remove absTerm appTerm appTerm 1533 def refl appThm nil 253 ref 1533 remove nil cons cons nil cons nil cons cons 295 ref subst trans absThm appThm 705 ref 1444 remove 1111 ref subst subst trans sym 66 ref eqMp eqMp 1534 def nil 1482 remove 1418 ref 39 ref 68 ref 1416 remove constTerm 1535 def 1424 remove appTerm appTerm 1524 ref 1527 remove appTerm appTerm absTerm 1536 def appTerm 1537 def thm 40 ref 0 ref 0 ref 0 ref 319 ref 1428 ref nil cons cons opType 1538 def 8 ref cons opType 8 ref cons opType constTerm 1539 def refl 1540 def "p" 1538 ref var 1541 def 132 ref 330 ref 1289 ref 1449 ref nil "t" 1428 remove var 1542 def 1541 ref varTerm 1543 def 1290 ref appTerm 1544 def nil cons cons nil cons nil cons cons 1457 remove 317 ref cons 35 ref cons 1273 ref subst 1545 def subst 1546 def appThm absThm appThm appThm 132 ref 1531 remove "h" 1414 ref var 1547 def 1547 ref 1543 ref "Function.o" const 1548 def 0 ref 1468 ref 0 ref 1414 ref 335 remove cons opType nil cons cons opType constTerm 1469 ref appTerm 1547 remove varTerm 1549 def appTerm appTerm 1548 ref 0 ref 1471 ref 0 ref 1414 ref 1456 ref cons opType nil cons cons opType constTerm 1472 ref appTerm 1549 ref appTerm appTerm absTerm 1550 def 1549 remove appTerm betaConv absThm 1551 def appThm appThm 330 ref 1426 ref 1449 ref 1431 ref 1550 ref 1435 ref appTerm betaConv absThm 1552 def appThm absThm appThm appThm nil 1418 remove 1550 ref nil cons cons nil cons nil cons cons 1553 def 1481 remove subst eqMp 330 ref 1426 ref 1449 remove 1431 remove 1543 ref refl nil "g" 1414 remove var 1450 remove cons 1554 def "f" 1468 ref var 1469 ref nil cons cons nil cons cons nil cons cons 1465 ref 194 ref "C" 4 ref cons nil cons 1555 def cons cons 35 ref cons nil 12 ref 0 ref 0 ref 1058 ref 0 ref 319 remove 1456 remove cons opType nil cons cons opType 1556 def 0 ref 1556 ref 8 ref cons opType nil cons cons opType constTerm 1548 remove 1556 remove constTerm appTerm "f" 1058 ref var 1557 def 1426 ref 49 ref 1557 remove varTerm 1558 def 1433 ref 156 ref appTerm 1559 def appTerm absTerm absTerm 1560 def absTerm 1561 def appTerm axiom 1558 ref refl appThm 1561 remove 1558 remove appTerm betaConv trans 1433 ref refl appThm 1560 remove 1433 ref appTerm betaConv trans 1562 def subst subst 49 ref 1469 ref refl 1563 def 1435 remove 156 ref appTerm betaConv 1564 def appThm nil "b" 1055 ref var 1565 def 1434 remove 156 ref appTerm nil cons cons "a" 3 ref var 1566 def 1559 ref nil cons cons nil cons cons nil cons cons 1567 def 1330 ref 172 ref cons 35 ref cons 200 ref subst 1568 def subst trans absThm nil 320 remove 1477 remove cons nil cons nil cons cons 1273 ref subst trans trans appThm nil 1554 remove "f" 1471 ref var 1472 ref nil cons cons nil cons cons nil cons cons 1465 ref 194 ref "C" 1056 ref cons nil cons cons cons 35 ref cons 1562 remove subst subst 49 ref 1472 ref refl 1569 def 1564 remove appThm 1567 remove 1332 ref 209 ref subst 1570 def subst trans absThm nil "t" 1427 ref var 1480 remove cons nil cons nil cons cons 194 ref 1331 ref cons 35 ref cons 1273 remove subst subst trans trans appThm absThm nil 1542 remove 1543 remove 1433 ref appTerm nil cons cons nil cons nil cons cons 1545 remove subst trans 1571 def appThm absThm appThm trans appThm nil 253 ref 329 ref 1289 ref 1430 ref 1544 ref appTerm absTerm appTerm nil cons cons nil cons nil cons cons 295 ref subst trans absThm appThm 705 ref "A" 1538 remove nil cons cons nil cons 35 ref cons 1111 ref subst subst 1572 def trans sym 66 ref eqMp nil 1539 ref 1541 ref 39 ref 329 ref 1289 ref 1430 remove "g" 1427 remove var 1573 def 1544 ref 1573 remove varTerm appTerm absTerm 1574 def appTerm absTerm appTerm appTerm 1419 remove 1550 ref appTerm appTerm absTerm appTerm thm 1540 remove 1541 ref 132 ref 1525 ref 1289 ref 1529 ref 1546 remove appThm absThm appThm appThm 132 ref 1535 ref refl 1551 remove appThm appThm 1525 ref 1426 ref 1529 ref 1552 remove appThm absThm appThm appThm 1553 remove 1536 ref 1421 ref appTerm 1575 def betaConv 1534 remove nil 90 ref 1537 remove nil cons cons 91 ref 1575 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 1443 remove 1417 remove 1536 remove nil cons cons "x" 1415 remove var 1421 remove nil cons cons nil cons cons nil cons cons 162 ref subst eqMp eqMp subst eqMp 1525 remove 1426 ref 1529 remove 1571 remove appThm absThm appThm trans appThm nil 253 ref 1524 ref 1289 ref 1526 ref 1544 remove appTerm absTerm appTerm nil cons cons nil cons nil cons cons 295 ref subst trans absThm appThm 1572 remove trans sym 66 ref eqMp nil 1539 remove 1541 remove 39 ref 1524 remove 1289 ref 1526 remove 1574 remove appTerm absTerm appTerm appTerm 1535 remove 1550 remove appTerm appTerm absTerm appTerm thm 1095 ref 1077 ref nil "g" 1073 ref var 1576 def 1206 ref "f'" 1073 ref var 1577 def 43 ref 70 ref 189 ref 74 ref 1209 ref 1577 ref varTerm 79 ref appTerm appTerm 1578 def 1079 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1579 def nil cons 1580 def cons 1077 ref 11 ref 1078 ref 22 ref appTerm 1581 def absTerm 1582 def nil cons cons nil cons cons nil cons cons 33 ref 1331 remove cons 35 ref cons 1426 ref 39 ref 322 remove 1290 ref appTerm 1433 ref appTerm 1583 def appTerm 43 ref 49 ref 202 ref 1291 remove appTerm 1559 remove appTerm absTerm appTerm 1584 def appTerm absTerm 1585 def 1433 remove appTerm 1586 def betaConv 1289 ref 329 ref 1585 ref appTerm 1587 def absTerm 1588 def 1290 remove appTerm 1589 def betaConv 330 ref 1289 ref 330 remove 1426 ref nil 1352 remove 1584 ref nil cons cons 253 ref 1583 ref nil cons cons nil cons cons nil cons cons 292 remove 954 remove 967 remove 961 remove 156 ref appTerm appTerm absTerm 1590 def 955 remove appTerm 1591 def betaConv 49 ref 43 ref 1590 ref appTerm 1592 def absTerm 1593 def 156 ref appTerm 1594 def betaConv nil 43 ref 1593 ref appTerm 1595 def axiom nil 90 ref 1595 remove nil cons cons 91 ref 1594 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 195 ref 44 ref 1593 remove nil cons cons 1257 ref cons nil cons cons 162 ref subst eqMp eqMp nil 90 ref 1592 remove nil cons cons 91 ref 1591 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 195 ref 44 ref 1590 remove nil cons cons 995 remove cons nil cons cons 162 ref subst eqMp eqMp subst subst absThm appThm absThm appThm sym nil 329 ref 1289 remove 329 ref 1426 remove 39 ref 1584 remove appTerm 1583 remove appTerm absTerm appTerm absTerm appTerm axiom eqMp nil 90 ref 329 remove 1588 ref appTerm nil cons cons 91 ref 1589 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 336 ref 337 ref 1588 remove nil cons cons 1298 remove cons nil cons cons 162 ref subst eqMp eqMp nil 90 ref 1587 remove nil cons cons 91 ref 1586 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 336 remove 337 remove 1585 remove nil cons cons 1478 remove cons nil cons cons 162 ref subst eqMp eqMp 1596 def subst 1597 def subst 132 ref 471 ref 11 ref 11 ref 1209 ref 1582 ref 22 ref appTerm appTerm 1579 ref 22 ref appTerm 1598 def appTerm absTerm 1599 def 22 ref appTerm betaConv absThm appThm appThm 313 ref 70 ref 490 ref 74 ref 1599 ref 79 ref appTerm betaConv absThm appThm absThm appThm appThm nil 261 ref 1599 remove nil cons cons nil cons nil cons cons 1402 ref subst eqMp trans 313 ref 70 ref 490 ref 74 ref 1240 ref nil 941 remove 835 remove cons nil cons nil cons cons 1330 remove 34 ref cons 35 ref cons 1299 ref subst subst appThm 74 ref 1209 ref 1206 ref "_1382" 1073 ref var 1600 def 43 ref 70 ref 189 ref 74 ref 1209 ref 1600 remove varTerm 79 ref appTerm appTerm 1079 ref appTerm absTerm appTerm absTerm appTerm absTerm 1601 def appTerm 1602 def 79 ref appTerm appTerm 1079 ref appTerm absTerm 1603 def 78 ref appTerm 1604 def betaConv 70 ref 189 ref 1603 ref appTerm 1605 def absTerm 1606 def 76 ref appTerm 1607 def betaConv 1601 ref 1602 remove appTerm 1608 def betaConv 1601 ref "_1380" 6 ref var 1609 def 1078 ref 17 ref 1205 ref 0 ref 0 ref 20 ref 8 ref cons opType 1610 def 20 ref nil cons 1611 def cons opType constTerm "fn" 20 remove var 1612 def 43 ref 70 ref 189 ref 74 ref 186 ref 1612 ref varTerm 79 ref appTerm appTerm 1613 def 76 ref appTerm absTerm appTerm absTerm appTerm absTerm 1614 def appTerm 1615 def 1609 remove varTerm 1616 def appTerm appTerm 1205 ref 0 ref 0 ref 25 ref 8 ref cons opType 1617 def 25 ref nil cons 1618 def cons opType constTerm "fn" 25 remove var 1619 def 43 ref 70 ref 189 ref 74 ref 202 ref 1619 ref varTerm 79 ref appTerm appTerm 1620 def 78 ref appTerm absTerm appTerm absTerm appTerm absTerm 1621 def appTerm 1622 def 1616 remove appTerm appTerm appTerm absTerm 1623 def appTerm betaConv sym nil 44 ref 70 ref 189 ref 74 ref 1209 ref 1623 ref 79 ref appTerm 1624 def appTerm 1079 ref appTerm 1625 def absTerm 1626 def appTerm 1627 def absTerm nil cons cons nil cons nil cons cons 59 ref subst 70 ref nil 61 ref 1627 remove nil cons cons nil cons nil cons cons 67 ref subst nil 168 ref 1626 remove nil cons cons nil cons nil cons cons 174 ref subst 74 ref nil 61 ref 1625 remove nil cons cons nil cons nil cons cons 67 ref subst 1624 remove betaConv 1209 ref "_1377" 3 ref var 1628 def 1078 ref 77 remove 1628 ref varTerm 1629 def appTerm appTerm absTerm 78 ref appTerm 1630 def appTerm refl 1628 ref 1078 ref 17 ref 1615 ref 79 ref appTerm 1631 def appTerm 1632 def 1629 ref appTerm appTerm absTerm 1633 def 1622 ref 79 ref appTerm 1634 def appTerm betaConv appThm 1240 ref 1630 remove betaConv 1635 def appThm 1078 ref 1632 remove 1634 ref appTerm appTerm refl appThm trans 12 ref 0 ref 1058 ref 0 ref 1058 remove 8 ref cons opType nil cons cons opType constTerm 1636 def "_1376" 2 ref var 1637 def 1628 remove 1078 ref 17 ref 1637 remove varTerm appTerm 1629 remove appTerm appTerm absTerm absTerm 1638 def 76 ref appTerm 1639 def appTerm refl 1638 ref 1631 ref appTerm betaConv appThm 1636 remove refl 1639 remove betaConv 1640 def appThm 1633 remove refl appThm trans 1638 remove refl 74 ref 186 ref 1631 ref appTerm 76 ref appTerm absTerm 1641 def 78 ref appTerm 1642 def betaConv 70 ref 189 ref 1641 ref appTerm 1643 def absTerm 1644 def 76 ref appTerm 1645 def betaConv 1614 ref 1615 ref appTerm 1646 def betaConv 68 ref 0 ref 1610 ref 8 ref cons opType constTerm 1647 def refl 1612 remove 313 ref 70 ref 490 ref 74 ref 1613 remove refl 70 ref 74 ref 76 ref absTerm 1648 def absTerm 1649 def 76 ref appTerm betaConv 78 ref refl 1650 def appThm 1648 remove 78 ref appTerm betaConv trans appThm absThm appThm absThm appThm absThm appThm "C" 19 ref cons nil cons "_1371" 0 ref 2 ref 0 ref 3 ref 19 ref cons opType nil cons cons opType var 1649 remove nil cons cons nil cons nil cons cons nil 1066 ref 70 ref 74 ref "_1371" 1060 remove var varTerm 76 ref appTerm 78 ref appTerm 1651 def absTerm 1652 def absTerm 1653 def nil cons cons nil cons nil cons cons 1260 remove subst nil 90 ref 1261 ref 1235 ref 43 ref 70 ref 189 ref 74 ref 1237 ref 1653 remove 76 ref appTerm 1654 def 78 ref appTerm appTerm absTerm appTerm absTerm appTerm 1655 def absTerm 1656 def appTerm 1657 def nil cons cons 91 ref 1261 ref 1235 ref 43 ref 70 ref 189 ref 74 ref 1237 ref 1651 remove appTerm absTerm appTerm absTerm appTerm absTerm 1658 def appTerm 1659 def nil cons 1660 def cons nil cons 1661 def cons nil cons cons 152 ref subst nil 1214 ref 1235 ref 92 ref 1656 ref 1236 ref appTerm 1662 def appTerm 1659 ref appTerm 1663 def absTerm nil cons cons nil cons nil cons cons 1107 ref 59 ref subst 1664 def subst 1235 remove nil 61 ref 1663 remove nil cons cons nil cons nil cons cons 67 ref subst nil 90 ref 1662 ref nil cons 1665 def cons 1661 ref cons nil cons cons 1666 def 109 ref subst 1666 remove 160 ref subst 1662 ref betaConv 1662 remove assume eqMp nil 90 ref 1655 ref nil cons 1667 def cons 1661 remove cons nil cons cons 1668 def 152 ref subst proveHyp 1668 ref 109 ref subst 1668 remove 160 ref subst 1658 ref 1236 ref appTerm betaConv sym 313 ref 70 ref 490 ref 74 ref 1237 remove refl 1654 remove betaConv 1650 ref appThm 1652 remove 78 ref appTerm betaConv trans appThm absThm appThm absThm appThm 1655 remove assume eqMp eqMp 1106 ref 1214 ref 1658 remove nil cons cons 1216 ref 1236 remove nil cons cons nil cons cons nil cons cons 1259 ref subst proveHyp eqMp nil 128 ref 1667 remove cons 130 ref 1660 remove cons nil cons 1669 def cons nil cons cons 144 ref subst deductAntisym eqMp eqMp eqMp nil 128 ref 1665 remove cons 1669 ref cons nil cons cons 144 ref subst deductAntisym eqMp eqMp absThm eqMp nil 90 ref 1076 ref 1216 ref 92 ref 1656 ref 1216 ref varTerm appTerm appTerm 1659 ref appTerm absTerm appTerm nil cons cons 91 ref 92 ref 1657 remove appTerm 1659 remove appTerm nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 1106 ref 1214 ref 1656 remove nil cons cons 1669 remove cons nil cons cons 256 ref subst eqMp eqMp proveHyp 1670 def subst eqMp nil 90 ref 1647 remove 1614 ref appTerm nil cons cons 91 ref 1646 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp "A" 1611 remove cons nil cons "p" 1610 remove var 1614 remove nil cons cons nil cons nil cons cons 1328 ref subst eqMp eqMp nil 90 ref 43 ref 1644 ref appTerm nil cons cons 91 ref 1645 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 195 ref 44 ref 1644 remove nil cons cons 196 ref cons nil cons cons 162 ref subst eqMp eqMp nil 90 ref 1643 remove nil cons cons 91 ref 1642 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 172 ref 168 ref 1641 remove nil cons cons 199 ref cons nil cons cons 162 ref subst eqMp eqMp sym 1671 def appThm eqMp 74 ref 202 ref 1634 ref appTerm 78 ref appTerm absTerm 1672 def 78 ref appTerm 1673 def betaConv 70 ref 189 ref 1672 ref appTerm 1674 def absTerm 1675 def 76 ref appTerm 1676 def betaConv 1621 ref 1622 ref appTerm 1677 def betaConv 68 ref 0 ref 1617 ref 8 ref cons opType constTerm 1678 def refl 1619 remove 313 ref 70 ref 490 ref 74 ref 1620 remove refl 70 ref 74 ref 78 ref absTerm absTerm 1679 def 76 ref appTerm betaConv 1650 ref appThm "_1374" 3 ref var 1680 def 1680 remove varTerm absTerm 78 ref appTerm betaConv trans appThm absThm appThm absThm appThm absThm appThm 1555 remove "_1371" 0 ref 2 ref 0 ref 3 ref 4 ref cons opType nil cons cons opType var 1679 remove nil cons cons nil cons nil cons cons 1670 remove subst eqMp nil 90 ref 1678 remove 1621 ref appTerm nil cons cons 91 ref 1677 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp "A" 1618 remove cons nil cons "p" 1617 remove var 1621 remove nil cons cons nil cons nil cons cons 1328 ref subst eqMp eqMp nil 90 ref 43 ref 1675 ref appTerm nil cons cons 91 ref 1676 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 195 ref 44 ref 1675 remove nil cons cons 196 ref cons nil cons cons 162 ref subst eqMp eqMp nil 90 ref 1674 remove nil cons cons 91 ref 1673 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 172 ref 168 ref 1672 remove nil cons cons 199 ref cons nil cons cons 162 ref subst eqMp eqMp sym 1681 def appThm eqMp sym trans eqMp absThm eqMp eqMp absThm eqMp eqMp 1106 ref 1214 ref 1601 ref nil cons 1682 def cons 1216 ref 1623 remove nil cons cons nil cons cons nil cons cons 1259 ref subst proveHyp nil 90 ref 1261 ref 1601 remove appTerm nil cons cons 91 ref 1608 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp nil 1262 ref 1682 remove cons nil cons nil cons cons 1329 remove subst eqMp eqMp nil 90 ref 43 ref 1606 ref appTerm nil cons cons 91 ref 1607 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 195 ref 44 ref 1606 remove nil cons cons 196 ref cons nil cons cons 162 ref subst eqMp eqMp nil 90 ref 1605 remove nil cons cons 91 ref 1604 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 172 ref 168 ref 1603 remove nil cons cons 199 ref cons nil cons cons 162 ref subst eqMp eqMp 1683 def appThm nil 1243 ref 1079 ref nil cons cons nil cons nil cons cons 1247 remove subst 1684 def trans absThm appThm 1248 ref trans absThm appThm 1249 ref trans trans absThm appThm 1112 remove trans sym 66 ref eqMp 1685 def nil 1076 ref 1077 ref 12 ref 0 ref 1073 remove 1074 remove nil cons 1686 def cons opType constTerm 1687 def 1582 remove appTerm 1579 ref appTerm absTerm 1688 def appTerm 1689 def thm 1348 ref 1066 ref 1687 ref 1206 ref 1077 ref 43 ref 49 ref 189 ref 1390 ref 1209 ref 1078 ref 17 ref 156 ref appTerm 1393 ref appTerm appTerm appTerm 1068 ref 156 ref appTerm 1393 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1690 def appTerm 1691 def refl 1687 ref refl 11 ref 1239 remove 22 ref appTerm betaConv absThm appThm 1206 remove refl 1692 def 1577 ref 313 ref 70 ref 490 ref 74 ref 1578 remove refl 1693 def 1241 remove appThm absThm appThm absThm appThm absThm appThm appThm nil 1077 ref "p" 6 ref var 1694 def 1068 ref 21 ref 1694 ref varTerm 1695 def appTerm 1696 def appTerm 26 ref 1695 remove appTerm 1697 def appTerm absTerm 1698 def nil cons cons nil cons nil cons cons 1688 ref 1078 ref appTerm 1699 def betaConv 1685 remove nil 90 ref 1689 remove nil cons cons 91 ref 1699 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 1106 remove 1214 ref 1688 remove nil cons cons 1216 ref 1078 ref nil cons 1700 def cons nil cons cons nil cons cons 162 ref subst eqMp eqMp subst eqMp 1692 ref 1577 ref 313 ref 70 ref 490 ref 74 ref 1693 ref 1242 remove appThm absThm appThm absThm appThm absThm appThm trans appThm nil 1216 remove 1690 remove nil cons cons nil cons nil cons cons 1107 remove 294 ref subst subst trans absThm appThm 705 ref 1203 remove 1111 ref subst subst trans sym 66 ref eqMp 1701 def nil 1065 ref 1066 ref 1691 remove 1698 remove appTerm absTerm 1702 def appTerm 1703 def thm 40 ref 0 ref 1075 remove 8 ref cons opType constTerm 1704 def refl 1705 def 1262 ref 39 ref 1076 ref 1077 ref 1262 ref varTerm 1706 def 1078 ref appTerm absTerm 1707 def appTerm 1708 def appTerm 1709 def refl 132 ref 1348 remove 1066 ref 1066 remove 1706 ref 1212 remove appTerm absTerm 1710 def 1068 ref appTerm betaConv absThm 1711 def appThm appThm 1095 ref 1077 ref 1710 ref 1080 remove appTerm betaConv absThm 1712 def appThm appThm nil 1064 remove 1710 ref nil cons cons nil cons nil cons cons 1713 def 1340 remove subst eqMp 1095 remove 1077 ref 1706 remove refl 1692 remove 1577 remove 313 ref 70 ref 490 ref 74 ref 1693 remove 1640 remove 1650 remove appThm 1635 remove trans appThm absThm appThm absThm appThm absThm appThm nil 1576 remove 1700 remove cons 1077 ref 1580 remove cons nil cons cons nil cons cons 1597 remove subst 132 ref 471 ref 11 ref 11 ref 1209 ref 1598 remove appTerm 1581 remove appTerm absTerm 1714 def 22 ref appTerm betaConv absThm appThm appThm 313 ref 70 ref 490 ref 74 ref 1714 ref 79 ref appTerm betaConv absThm appThm absThm appThm appThm nil 261 ref 1714 remove nil cons cons nil cons nil cons cons 1402 ref subst eqMp trans 313 ref 70 ref 490 ref 74 ref 1240 ref 1683 remove appThm 1079 remove refl appThm 1684 remove trans absThm appThm 1248 ref trans absThm appThm 1249 ref trans trans 1715 def sym 66 ref eqMp trans appThm absThm 1716 def appThm trans appThm nil 253 ref 1708 remove nil cons cons nil cons nil cons cons 295 ref subst trans absThm appThm 705 ref "A" 1686 remove cons nil cons 35 ref cons 1111 ref subst subst 1717 def trans sym 66 ref eqMp nil 1704 ref 1262 ref 1709 remove 1065 remove 1710 ref appTerm appTerm absTerm appTerm thm 1705 remove 1262 ref 39 ref 1261 remove 1707 remove appTerm 1718 def appTerm 1719 def refl 132 ref 1342 ref refl 1711 remove appThm appThm 1350 ref 1712 remove appThm appThm 1713 remove 1382 remove subst eqMp 1350 remove 1716 remove appThm trans appThm nil 253 ref 1718 remove nil cons cons nil cons nil cons cons 295 ref subst trans absThm appThm 1717 remove trans sym 66 ref eqMp nil 1704 remove 1262 remove 1719 remove 1342 remove 1710 remove appTerm appTerm absTerm appTerm thm nil "P" 1386 remove var 1720 def 1389 ref 39 ref 88 ref 1205 ref 0 ref 87 ref 13 remove cons opType constTerm 1721 def "f" 9 ref var 1722 def 43 ref 70 ref 189 ref 74 ref 39 ref 1722 ref varTerm 79 ref appTerm appTerm 1391 ref 76 ref appTerm 1723 def 78 ref appTerm 1724 def appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1725 def appTerm appTerm 43 ref 70 ref 189 ref 74 ref 1724 ref absTerm 1726 def appTerm absTerm appTerm 1727 def appTerm 1728 def absTerm 1729 def nil cons cons nil cons nil cons cons 1406 remove 59 ref subst 1730 def subst 1389 ref nil 61 ref 1728 remove nil cons cons nil cons nil cons cons 67 ref subst 132 ref 36 ref 56 ref subst 1725 ref refl appThm appThm 1727 remove refl appThm sym 261 ref 12 ref 0 ref 9 ref 87 remove nil cons cons opType constTerm 1731 def 262 remove appTerm 11 ref 50 ref absTerm 1732 def appTerm absTerm 1725 ref appTerm betaConv nil "g" 9 ref var 1732 ref nil cons cons 1722 remove 1725 ref nil cons 1733 def cons nil cons cons nil cons cons 33 remove 317 ref cons 35 ref cons 1596 ref subst subst 132 ref 471 ref 11 ref 11 ref 39 ref 1725 ref 22 ref appTerm 1734 def appTerm 1732 ref 22 ref appTerm appTerm absTerm 1735 def 22 ref appTerm betaConv absThm appThm appThm 313 ref 70 ref 490 ref 74 ref 1735 ref 79 ref appTerm betaConv absThm appThm absThm appThm appThm nil 261 ref 1735 remove nil cons cons nil cons nil cons cons 1402 ref subst eqMp trans trans 313 ref 70 ref 490 ref 74 ref 132 ref 74 ref 39 ref 1721 remove "_1510" 9 ref var 1736 def 43 ref 70 ref 189 ref 74 ref 39 ref 1736 remove varTerm 79 ref appTerm appTerm 1724 ref appTerm absTerm appTerm absTerm appTerm absTerm 1737 def appTerm 1738 def 79 ref appTerm appTerm 1724 ref appTerm absTerm 1739 def 78 ref appTerm 1740 def betaConv 70 ref 189 ref 1739 ref appTerm 1741 def absTerm 1742 def 76 ref appTerm 1743 def betaConv 1737 ref 1738 remove appTerm 1744 def betaConv 1737 ref "_1508" 6 remove var 1745 def 1391 ref 1615 remove 1745 remove varTerm 1746 def appTerm appTerm 1622 remove 1746 remove appTerm appTerm absTerm 1747 def appTerm betaConv sym nil 44 ref 70 ref 189 ref 74 ref 39 ref 1747 ref 79 ref appTerm 1748 def appTerm 1724 ref appTerm 1749 def absTerm 1750 def appTerm 1751 def absTerm nil cons cons nil cons nil cons cons 59 ref subst 70 ref nil 61 ref 1751 remove nil cons cons nil cons nil cons cons 67 ref subst nil 168 ref 1750 remove nil cons cons nil cons nil cons cons 174 ref subst 74 ref nil 61 ref 1749 remove nil cons cons nil cons nil cons cons 67 ref subst 1748 remove betaConv 39 ref "_1505" 3 ref var 1752 def 1723 remove 1752 ref varTerm 1753 def appTerm absTerm 78 ref appTerm 1754 def appTerm refl 1752 ref 1391 ref 1631 ref appTerm 1755 def 1753 ref appTerm absTerm 1756 def 1634 ref appTerm betaConv appThm 132 ref 1754 remove betaConv appThm 1755 remove 1634 remove appTerm refl appThm trans 12 ref 0 ref 71 remove 72 remove nil cons cons opType constTerm 1757 def "_1504" 2 ref var 1758 def 1752 remove 1391 ref 1758 remove varTerm appTerm 1753 remove appTerm absTerm absTerm 1759 def 76 ref appTerm 1760 def appTerm refl 1759 ref 1631 remove appTerm betaConv appThm 1757 remove refl 1760 remove betaConv appThm 1756 remove refl appThm trans 1759 remove refl 1671 ref appThm eqMp 1681 ref appThm eqMp sym trans eqMp absThm eqMp eqMp absThm eqMp eqMp 310 remove 308 ref 1737 ref nil cons 1761 def cons 844 remove 1747 remove nil cons cons nil cons cons nil cons cons 1259 ref subst proveHyp nil 90 ref 358 remove 1737 remove appTerm nil cons cons 91 ref 1744 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp nil 503 remove 1761 remove cons nil cons nil cons cons 311 remove 1328 ref subst subst eqMp eqMp nil 90 ref 43 ref 1742 ref appTerm nil cons cons 91 ref 1743 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 195 ref 44 ref 1742 remove nil cons cons 196 ref cons nil cons cons 162 ref subst eqMp eqMp nil 90 ref 1741 remove nil cons cons 91 ref 1740 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 172 ref 168 ref 1739 remove nil cons cons 199 ref cons nil cons cons 162 ref subst eqMp eqMp 1762 def appThm 1732 remove 79 ref appTerm betaConv appThm nil 61 ref 1724 ref nil cons cons nil cons nil cons cons 61 ref 39 ref 65 remove appTerm 63 ref appTerm absTerm 1763 def 63 remove appTerm 1764 def betaConv nil 230 remove 1763 ref appTerm 1765 def axiom nil 90 ref 1765 remove nil cons cons 91 ref 1764 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 251 remove 252 remove 1763 remove nil cons cons 284 remove cons nil cons cons 162 ref subst eqMp eqMp 1766 def subst trans absThm appThm absThm appThm trans eqMp eqMp absThm eqMp nil 1387 ref 1729 remove appTerm thm nil 1720 ref 1389 ref 39 ref 487 ref 1725 ref appTerm 1767 def appTerm 69 ref 70 ref 73 ref 1726 remove appTerm absTerm 1768 def appTerm 1769 def appTerm 1770 def absTerm 1771 def nil cons cons nil cons nil cons cons 1730 ref subst 1389 ref nil 61 ref 1770 remove nil cons 1772 def cons nil cons nil cons cons 67 ref subst 132 ref nil 261 ref 1733 remove cons nil cons nil cons cons 36 ref 47 ref 39 ref 275 ref 1263 remove appTerm appTerm 861 remove appTerm absTerm 1773 def 48 remove appTerm 1774 def betaConv 349 ref refl 47 ref 132 ref 312 ref 1274 remove appThm appThm 313 ref 49 ref 345 remove refl absThm appThm appThm absThm appThm 865 remove eqMp nil 90 ref 349 remove 1773 ref appTerm nil cons cons 91 ref 1774 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 351 ref 352 remove 1773 remove nil cons cons 355 remove cons nil cons cons 162 ref subst eqMp eqMp 1775 def subst subst 132 ref 471 ref 11 ref 11 ref 275 ref 1734 remove appTerm absTerm 1776 def 22 ref appTerm betaConv absThm appThm appThm 313 ref 70 ref 490 ref 74 ref 1776 ref 79 ref appTerm betaConv absThm appThm absThm appThm appThm nil 261 remove 1776 remove nil cons cons nil cons nil cons cons 1402 ref subst eqMp trans 313 ref 70 ref 490 ref 74 ref 312 ref 1762 remove appThm absThm appThm absThm appThm trans appThm nil 47 ref 1768 ref nil cons 1777 def cons nil cons nil cons cons 1775 ref subst 313 ref 49 ref 312 ref 1768 ref 156 ref appTerm 1778 def betaConv appThm nil 574 ref 74 ref 1392 remove 78 ref appTerm absTerm 1779 def nil cons cons nil cons nil cons cons 173 remove 1775 ref subst 1780 def subst 490 ref 197 ref 312 ref 1779 remove 211 ref appTerm betaConv appThm absThm appThm trans trans absThm appThm trans 1781 def appThm nil 253 ref 43 ref 70 ref 189 ref 74 ref 275 ref 1724 ref appTerm absTerm appTerm absTerm 1782 def appTerm nil cons 1783 def cons nil cons nil cons cons 295 ref subst trans sym 66 ref eqMp nil 90 ref 39 ref 275 ref 1767 ref appTerm appTerm 275 ref 1769 ref appTerm 1784 def appTerm nil cons cons 91 ref 1772 remove cons nil cons cons nil cons cons 152 ref subst proveHyp nil 91 ref 1769 ref nil cons 1785 def cons 90 ref 1767 remove nil cons cons nil cons cons nil cons cons nil 368 remove 91 ref 92 ref 830 remove 370 ref appTerm appTerm 240 remove appTerm nil cons 1786 def cons nil cons 1787 def cons nil cons cons 1788 def 109 ref subst 1788 remove 160 ref subst 39 ref "_1514" 7 ref var 1789 def 92 ref 39 ref 275 ref 1789 remove varTerm 1790 def appTerm appTerm 370 ref appTerm appTerm 39 ref 1790 remove appTerm 95 ref appTerm appTerm absTerm 1791 def 93 remove appTerm 1792 def appTerm refl 1793 def 1791 ref 279 remove appTerm betaConv appThm 132 ref 1792 remove betaConv appThm 1794 def 92 ref 401 remove 370 ref appTerm appTerm 381 remove appTerm refl appThm trans 1791 remove refl 1795 def 386 remove appThm eqMp sym 713 ref 1369 remove 370 ref refl 1796 def appThm 395 ref 431 remove subst trans appThm 391 remove appThm 395 ref 827 ref subst trans sym 66 ref eqMp eqMp eqMp nil 415 remove 130 ref 1786 ref cons nil cons 1797 def cons nil cons cons 144 ref subst deductAntisym eqMp nil 419 remove 1787 remove cons nil cons cons 1798 def 109 ref subst 1798 remove 160 ref subst 1793 remove "_1512" 7 remove var 1799 def 92 ref 39 ref 275 ref 1799 remove varTerm 1800 def appTerm appTerm 370 ref appTerm appTerm 39 ref 1800 remove appTerm 95 remove appTerm appTerm absTerm 50 ref appTerm betaConv appThm 1794 remove 92 ref 433 remove 370 remove appTerm appTerm 424 remove appTerm refl appThm trans 1795 remove 427 remove appThm eqMp sym 713 ref 1379 remove 1796 remove appThm 395 remove 390 remove subst 392 remove trans trans appThm 432 remove appThm 125 remove 827 remove subst trans sym 66 ref eqMp eqMp eqMp nil 441 ref 1797 remove cons nil cons cons 144 ref subst deductAntisym eqMp 448 remove nil 441 remove 449 remove 450 remove 1786 remove cons nil cons cons cons nil cons cons 469 remove subst proveHyp proveHyp proveHyp 1801 def subst eqMp eqMp absThm eqMp nil 1387 ref 1771 remove appTerm thm 1388 ref 1389 ref 14 ref refl 1205 ref 0 ref 9 ref 16 ref cons opType constTerm 1802 def refl nil "f" 1385 ref var 1391 ref nil cons 1803 def cons nil cons nil cons cons 194 ref "B" 4 ref cons "C" 8 ref cons nil cons cons cons 35 ref cons 1702 ref 1068 remove appTerm 1804 def betaConv 1701 remove nil 90 ref 1703 remove nil cons cons 91 ref 1804 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 1100 remove 1101 remove 1702 remove nil cons cons 1104 remove cons nil cons cons 162 ref subst eqMp eqMp subst subst 1805 def appThm appThm 1802 ref 11 ref 1391 ref 23 remove appTerm 27 remove appTerm 1806 def absTerm 1807 def appTerm 1808 def refl appThm nil 11 ref 1802 ref 1694 remove 1391 ref 1696 remove appTerm 1697 remove appTerm absTerm appTerm nil cons cons nil cons nil cons cons 36 remove 294 ref subst subst trans absThm appThm 1407 remove trans sym 66 ref eqMp nil 1387 ref 1389 ref 14 ref 1802 ref 1725 ref appTerm 1809 def appTerm 1808 ref appTerm absTerm appTerm thm 40 ref 0 ref 0 ref 0 ref 1 ref 1413 remove opType 1810 def "D" varType 1811 def nil cons 1812 def cons opType 1813 def 8 ref cons opType 1814 def 8 ref cons opType 1815 def constTerm 1816 def refl "f" 1813 ref var 1817 def nil "g" 1813 ref var 1818 def 1205 ref 0 ref 1814 ref 1813 ref nil cons 1819 def cons opType constTerm 1820 def "f'" 1813 ref var 1821 def 43 ref 49 ref 189 ref 1390 ref 40 ref 0 ref 1207 ref 8 ref cons opType 1822 def constTerm 1823 def "z" 1055 ref var 1824 def 12 ref 0 ref 1811 ref 0 ref 1811 ref 8 ref cons opType 1825 def nil cons cons opType constTerm 1826 def 1821 ref varTerm 1827 def 15 ref 0 ref 2 ref 0 ref 1411 ref 1810 ref nil cons 1828 def cons opType nil cons cons opType constTerm 1829 def 156 ref appTerm 1830 def 1432 ref 1393 ref appTerm 1831 def 1824 ref varTerm 1832 def appTerm 1833 def appTerm 1834 def appTerm appTerm 1835 def 1817 ref varTerm 1836 def 1834 ref appTerm 1837 def appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1838 def nil cons cons 1817 ref "t" 1810 ref var 1839 def 1836 ref 1839 ref varTerm 1840 def appTerm absTerm 1841 def nil cons cons nil cons cons nil cons cons "A" 1828 remove cons 1842 def "B" 1812 ref cons 1843 def nil cons 1844 def cons 35 ref cons 1596 ref subst 1845 def subst 132 ref 40 ref 0 ref 0 ref 1810 ref 8 ref cons opType 1846 def 8 ref cons opType 1847 def constTerm 1848 def refl 1849 def "x" 1810 ref var 1850 def 1850 ref 1826 ref 1841 ref 1850 ref varTerm 1851 def appTerm appTerm 1838 ref 1851 ref appTerm appTerm absTerm 1852 def 1851 ref appTerm betaConv absThm appThm appThm 313 ref 70 ref 40 ref 0 ref 0 ref 1411 ref 8 ref cons opType 1853 def 8 ref cons opType constTerm 1854 def refl 1855 def "b" 1411 ref var 1856 def 1852 ref 1829 ref 76 ref appTerm 1857 def 1856 ref varTerm 1858 def appTerm 1859 def appTerm betaConv absThm appThm absThm appThm appThm nil "p" 1846 ref var 1860 def 1852 remove nil cons cons nil cons nil cons cons 1466 ref 1402 ref subst 1861 def subst eqMp trans 313 ref 70 ref 132 ref 1855 ref 1856 ref 1856 ref 1826 ref 1841 ref 1859 ref appTerm appTerm 1838 ref 1859 ref appTerm appTerm absTerm 1862 def 1858 ref appTerm betaConv absThm appThm appThm 490 ref 1566 ref 1823 ref refl 1863 def 1565 ref 1862 ref 1432 ref 1566 ref varTerm 1864 def appTerm 1565 ref varTerm 1865 def appTerm 1866 def appTerm betaConv absThm appThm absThm appThm appThm nil "p" 1853 ref var 1867 def 1862 remove nil cons cons nil cons nil cons cons 1332 ref 1402 ref subst 1868 def subst eqMp 490 ref 1566 ref 1863 ref 1565 ref 1826 ref refl 1869 def nil "y" 1810 ref var 1857 ref 1866 ref appTerm 1870 def nil cons cons nil cons nil cons cons 1843 remove 1842 ref nil cons 1871 def cons 35 ref cons 1299 remove subst subst appThm nil 1824 ref 1865 ref nil cons 1872 def cons 1390 ref 1864 ref nil cons 1873 def cons 196 ref cons cons nil cons cons 1824 ref 1826 ref 1820 ref "_1404" 1813 ref var 1874 def 43 ref 49 ref 189 ref 1390 ref 1823 ref 1824 ref 1826 ref 1874 remove varTerm 1834 ref appTerm appTerm 1837 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 1875 def appTerm 1876 def 1834 ref appTerm appTerm 1837 ref appTerm absTerm 1877 def 1832 ref appTerm 1878 def betaConv 1390 ref 1823 ref 1877 ref appTerm 1879 def absTerm 1880 def 1393 ref appTerm 1881 def betaConv 49 ref 189 ref 1880 ref appTerm 1882 def absTerm 1883 def 156 ref appTerm 1884 def betaConv 1875 ref 1876 remove appTerm 1885 def betaConv 1875 ref "_1402" 1810 ref var 1886 def 1836 ref 1829 ref 1205 ref 0 ref 0 ref 0 ref 1810 ref 19 ref cons opType 1887 def 8 ref cons opType 1887 ref nil cons cons opType constTerm "fn" 1887 ref var 1888 def 43 ref 70 ref 1854 ref 1856 ref 186 ref 1888 remove varTerm 1859 ref appTerm appTerm 76 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1889 def 1886 remove varTerm 1890 def appTerm appTerm 1432 ref 1205 ref 0 ref 0 ref 1468 ref 8 ref cons opType 1468 ref nil cons cons opType constTerm "fn" 1468 remove var 1891 def 189 ref 1566 ref 1823 ref 1565 ref 202 ref 1891 remove varTerm 1866 ref appTerm appTerm 1864 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1892 def 1205 ref 0 ref 0 ref 0 ref 1810 ref 1412 remove cons opType 1893 def 8 ref cons opType 1893 ref nil cons cons opType constTerm "fn" 1893 ref var 1894 def 43 ref 70 ref 1854 remove 1856 ref 12 ref 0 ref 1411 ref 1853 remove nil cons cons opType constTerm 1894 remove varTerm 1859 ref appTerm appTerm 1858 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1895 def 1890 remove appTerm 1896 def appTerm appTerm 1205 ref 0 ref 0 ref 1471 ref 8 ref cons opType 1471 ref nil cons cons opType constTerm "fn" 1471 remove var 1897 def 189 ref 1566 ref 1823 ref 1565 ref 1209 ref 1897 remove varTerm 1866 ref appTerm appTerm 1865 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1898 def 1896 remove appTerm appTerm appTerm appTerm absTerm 1899 def appTerm betaConv sym nil 44 ref 49 ref 189 ref 1390 ref 1823 ref 1824 ref 1826 ref 1899 ref 1834 ref appTerm 1900 def appTerm 1837 ref appTerm 1901 def absTerm 1902 def appTerm 1903 def absTerm 1904 def appTerm 1905 def absTerm nil cons cons nil cons nil cons cons 59 ref subst 49 ref nil 61 ref 1905 remove nil cons cons nil cons nil cons cons 67 ref subst nil 168 ref 1904 remove nil cons cons nil cons nil cons cons 174 ref subst 1390 ref nil 61 ref 1903 remove nil cons cons nil cons nil cons cons 67 ref subst nil "P" 1207 ref var 1906 def 1902 remove nil cons cons nil cons nil cons cons 1246 ref 59 ref subst 1907 def subst 1824 ref nil 61 ref 1901 remove nil cons cons nil cons nil cons cons 67 ref subst 1900 remove betaConv 1826 ref "_1398" 1055 ref var 1908 def 1836 ref 1830 ref 1831 remove 1908 ref varTerm 1909 def appTerm appTerm appTerm absTerm 1832 ref appTerm 1910 def appTerm refl 1908 ref 1836 ref 1829 ref 1889 ref 1834 ref appTerm 1911 def appTerm 1912 def 1432 ref 1892 ref 1895 ref 1834 ref appTerm 1913 def appTerm 1914 def appTerm 1915 def 1909 ref appTerm appTerm appTerm absTerm 1916 def 1898 ref 1913 ref appTerm 1917 def appTerm betaConv appThm 1869 ref 1910 remove betaConv appThm 1836 ref 1912 ref 1915 remove 1917 ref appTerm appTerm appTerm refl appThm trans 12 ref 0 ref 0 ref 1055 ref 1812 ref cons 1918 def opType 1919 def 0 ref 1919 ref 8 ref cons opType nil cons cons opType constTerm 1920 def "_1397" 3 ref var 1921 def 1908 ref 1836 ref 1830 remove 1432 ref 1921 ref varTerm appTerm 1909 remove appTerm 1922 def appTerm appTerm absTerm absTerm 1393 ref appTerm 1923 def appTerm refl 1921 ref 1908 ref 1836 ref 1912 remove 1922 ref appTerm appTerm absTerm absTerm 1924 def 1914 ref appTerm betaConv appThm 1920 remove refl 1923 remove betaConv appThm 1916 remove refl appThm trans 12 ref 0 ref 0 ref 3 ref 1919 remove nil cons cons opType 1925 def 0 ref 1925 ref 8 ref cons opType nil cons cons opType constTerm 1926 def "_1396" 2 ref var 1927 def 1921 remove 1908 remove 1836 ref 1829 remove 1927 remove varTerm appTerm 1922 remove appTerm appTerm absTerm absTerm absTerm 1928 def 156 ref appTerm 1929 def appTerm refl 1928 ref 1911 remove appTerm betaConv appThm 1926 remove refl 1929 remove betaConv appThm 1924 remove refl appThm trans 1928 remove refl nil 1856 ref 1833 ref nil cons cons 70 ref 1256 remove cons nil cons cons nil cons cons 1930 def 1466 ref 1671 ref subst 1931 def subst appThm eqMp 202 ref 1393 ref appTerm refl 202 ref "_1392" 1411 ref var 1932 def 1892 ref 1932 remove varTerm appTerm absTerm 1933 def 1833 ref appTerm 1934 def appTerm refl 1933 ref 1913 ref appTerm betaConv appThm 202 ref refl 1935 def 1934 remove betaConv appThm 1914 remove refl appThm trans 1933 remove refl 1936 def 1930 ref 1466 ref 1681 ref subst 1937 def subst 1938 def appThm eqMp appThm nil 1565 ref 1832 ref nil cons 1939 def cons 1566 ref 1393 ref nil cons 1940 def cons nil cons cons nil cons cons 1941 def 1332 ref 1671 ref subst 1942 def subst eqMp appThm eqMp 1209 ref 1832 ref appTerm refl 1209 ref "_1394" 1411 ref var 1943 def 1898 ref 1943 remove varTerm appTerm absTerm 1944 def 1833 remove appTerm 1945 def appTerm refl 1944 ref 1913 remove appTerm betaConv appThm 1240 ref 1945 remove betaConv appThm 1917 remove refl appThm trans 1944 remove refl 1946 def 1938 remove appThm eqMp appThm 1941 ref 1332 remove 1681 ref subst 1947 def subst eqMp appThm eqMp sym trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp "A" 1819 remove cons nil cons 1948 def "P" 1814 ref var 1949 def 1875 ref nil cons 1950 def cons "x" 1813 ref var 1951 def 1899 remove nil cons cons nil cons cons nil cons cons 1259 ref subst proveHyp nil 90 ref 68 ref 1815 remove constTerm 1875 remove appTerm nil cons cons 91 ref 1885 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp nil "p" 1814 ref var 1950 remove cons nil cons nil cons cons 1948 ref 35 ref cons 1952 def 1328 ref subst subst eqMp eqMp nil 90 ref 43 ref 1883 ref appTerm nil cons cons 91 ref 1884 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 195 ref 44 ref 1883 remove nil cons cons 1257 remove cons nil cons cons 162 ref subst eqMp eqMp nil 90 ref 1882 remove nil cons cons 91 ref 1881 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 172 ref 168 ref 1880 remove nil cons cons 197 ref 1940 remove cons nil cons cons nil cons cons 162 ref subst eqMp eqMp nil 90 ref 1879 remove nil cons cons 91 ref 1878 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 1245 ref 1906 ref 1877 remove nil cons cons 1243 ref 1939 remove cons nil cons cons nil cons cons 162 ref subst eqMp eqMp subst 1953 def appThm nil "x" 1811 ref var 1954 def 1836 ref 1870 ref appTerm 1955 def nil cons cons nil cons nil cons cons "A" 1812 ref cons nil cons 1956 def 35 ref cons 1957 def 294 ref subst subst 1958 def trans absThm appThm 705 ref 1246 ref 1111 ref subst subst 1959 def trans absThm appThm 1248 ref trans trans absThm appThm 1249 ref trans trans absThm appThm 705 ref 1952 ref 1111 ref subst subst trans sym 66 ref eqMp 1960 def nil 1816 ref 1817 ref 12 ref 0 ref 1813 remove 1814 remove nil cons cons opType constTerm 1961 def 1841 remove appTerm 1838 remove appTerm absTerm 1962 def appTerm 1963 def thm 40 ref 0 ref 0 ref 0 ref 2 ref 1925 remove nil cons cons opType 1964 def 8 ref cons opType 8 ref cons opType constTerm 1965 def refl "f" 1964 ref var 1966 def 1961 ref 1820 ref 1817 ref 43 ref 49 ref 189 ref 1390 ref 1823 ref 1824 ref 1826 ref 1837 remove appTerm 1966 ref varTerm 1967 def 156 ref appTerm 1393 remove appTerm 1832 remove appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1968 def appTerm 1969 def refl 1961 ref refl 1839 ref 1839 remove 1967 ref 18 remove 1887 remove constTerm 1840 ref appTerm appTerm 1469 remove 24 remove 1893 remove constTerm 1840 ref appTerm 1970 def appTerm appTerm 1472 remove 1970 remove appTerm appTerm absTerm 1971 def 1840 remove appTerm betaConv absThm appThm 1820 ref refl 1972 def 1821 ref 313 ref 49 ref 490 ref 1390 ref 1863 ref 1824 ref 1835 remove refl 1973 def 1971 ref 1834 remove appTerm betaConv appThm absThm appThm absThm appThm absThm appThm absThm appThm appThm nil 1817 ref 1971 ref nil cons cons nil cons nil cons cons 1962 ref 1836 ref appTerm 1974 def betaConv 1960 remove nil 90 ref 1963 remove nil cons cons 91 ref 1974 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 1948 remove 1949 ref 1962 remove nil cons cons 1951 ref 1836 ref nil cons 1975 def cons nil cons cons nil cons cons 162 ref subst eqMp eqMp subst eqMp 1972 remove 1821 ref 313 ref 49 ref 490 ref 1390 remove 1863 ref 1824 remove 1973 remove 1967 remove refl 1930 ref 1465 remove 195 ref cons 35 ref cons 200 remove subst subst appThm 1563 remove 1930 remove 1466 remove 209 remove subst subst 1976 def appThm 1941 ref 1568 remove subst trans appThm 1569 remove 1976 remove appThm 1941 remove 1570 remove subst trans appThm appThm absThm appThm absThm appThm absThm appThm absThm appThm trans appThm nil 1951 remove 1968 remove nil cons cons nil cons nil cons cons 1952 ref 294 ref subst subst trans absThm appThm 705 ref "A" 1964 remove nil cons cons nil cons 35 ref cons 1111 ref subst subst trans sym 66 ref eqMp nil 1965 remove 1966 remove 1969 remove 1971 remove appTerm absTerm appTerm thm nil "P" 0 ref 0 ref 2 ref 0 ref 3 ref 1208 remove cons opType 1977 def nil cons cons opType 1978 def 8 ref cons opType 1979 def var 1980 def "p" 1978 ref var 1981 def 39 ref 1848 remove 1205 ref 0 ref 1847 ref 1846 ref nil cons 1982 def cons opType constTerm 1983 def "f" 1846 ref var 1984 def 43 ref 70 ref 189 ref 74 ref 1823 ref "c" 1055 ref var 1985 def 39 ref 1984 ref varTerm 1857 remove 1432 remove 78 ref appTerm 1985 ref varTerm 1986 def appTerm 1987 def appTerm 1988 def appTerm appTerm 1981 ref varTerm 1989 def 76 ref appTerm 1990 def 78 ref appTerm 1991 def 1986 ref appTerm 1992 def appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1993 def appTerm appTerm 43 ref 70 ref 189 ref 74 ref 1823 ref 1985 ref 1992 ref absTerm 1994 def appTerm absTerm appTerm absTerm appTerm 1995 def appTerm 1996 def absTerm 1997 def nil cons cons nil cons nil cons cons "A" 1978 remove nil cons cons nil cons 35 ref cons 59 ref subst 1998 def subst 1981 ref nil 61 ref 1996 remove nil cons cons nil cons nil cons cons 67 ref subst 132 ref 1871 remove 35 ref cons 1999 def 56 remove subst 1993 ref refl appThm appThm 1995 remove refl appThm sym 1860 ref 12 ref 0 ref 1846 ref 1847 ref nil cons cons opType constTerm 1860 ref varTerm appTerm 1850 ref 50 remove absTerm 2000 def appTerm absTerm 1993 ref appTerm betaConv nil "g" 1846 ref var 2000 ref nil cons cons 1984 remove 1993 ref nil cons 2001 def cons nil cons cons nil cons cons 1842 remove 317 remove cons 35 ref cons 1596 ref subst subst 132 ref 1849 ref 1850 ref 1850 ref 39 ref 1993 ref 1851 ref appTerm 2002 def appTerm 2000 ref 1851 ref appTerm appTerm absTerm 2003 def 1851 ref appTerm betaConv absThm appThm appThm 313 ref 70 ref 1855 ref 1856 ref 2003 ref 1859 ref appTerm betaConv absThm appThm absThm appThm appThm nil 1860 ref 2003 remove nil cons cons nil cons nil cons cons 1861 ref subst eqMp trans trans 313 ref 70 ref 132 ref 1855 ref 1856 ref 1856 ref 39 ref 1993 ref 1859 ref appTerm 2004 def appTerm 2000 ref 1859 ref appTerm appTerm absTerm 2005 def 1858 ref appTerm betaConv absThm appThm appThm 490 ref 1566 ref 1863 ref 1565 ref 2005 ref 1866 ref appTerm betaConv absThm appThm absThm appThm appThm nil 1867 ref 2005 remove nil cons cons nil cons nil cons cons 1868 ref subst eqMp 490 ref 1566 ref 1863 ref 1565 ref 132 ref nil 1985 ref 1872 remove cons 74 ref 1873 remove cons nil cons 2006 def cons nil cons cons 1985 ref 39 ref 1983 remove "_1548" 1846 ref var 2007 def 43 ref 70 ref 189 ref 74 ref 1823 ref 1985 ref 39 ref 2007 remove varTerm 1988 ref appTerm appTerm 1992 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 2008 def appTerm 2009 def 1988 ref appTerm appTerm 1992 ref appTerm absTerm 2010 def 1986 ref appTerm 2011 def betaConv 74 ref 1823 ref 2010 ref appTerm 2012 def absTerm 2013 def 78 ref appTerm 2014 def betaConv 70 ref 189 ref 2013 ref appTerm 2015 def absTerm 2016 def 76 ref appTerm 2017 def betaConv 2008 ref 2009 remove appTerm 2018 def betaConv 2008 ref "_1546" 1810 remove var 2019 def 1989 ref 1889 ref 2019 remove varTerm 2020 def appTerm appTerm 1892 ref 1895 ref 2020 remove appTerm 2021 def appTerm appTerm 1898 ref 2021 remove appTerm appTerm absTerm 2022 def appTerm betaConv sym nil 44 ref 70 ref 189 ref 74 ref 1823 ref 1985 ref 39 ref 2022 ref 1988 ref appTerm 2023 def appTerm 1992 remove appTerm 2024 def absTerm 2025 def appTerm 2026 def absTerm 2027 def appTerm 2028 def absTerm nil cons cons nil cons nil cons cons 59 ref subst 70 ref nil 61 ref 2028 remove nil cons cons nil cons nil cons cons 67 ref subst nil 168 ref 2027 remove nil cons cons nil cons nil cons cons 174 ref subst 74 ref nil 61 ref 2026 remove nil cons cons nil cons nil cons cons 67 ref subst nil 1906 ref 2025 remove nil cons cons nil cons nil cons cons 1907 ref subst 1985 ref nil 61 ref 2024 remove nil cons cons nil cons nil cons cons 67 ref subst 2023 remove betaConv 39 ref "_1542" 1055 ref var 2029 def 1991 remove 2029 ref varTerm 2030 def appTerm absTerm 1986 ref appTerm 2031 def appTerm refl 2029 ref 1989 ref 1889 remove 1988 ref appTerm 2032 def appTerm 2033 def 1892 ref 1895 remove 1988 ref appTerm 2034 def appTerm 2035 def appTerm 2036 def 2030 ref appTerm absTerm 2037 def 1898 ref 2034 ref appTerm 2038 def appTerm betaConv appThm 132 ref 2031 remove betaConv appThm 2036 remove 2038 ref appTerm refl appThm trans 12 ref 0 ref 1207 ref 1822 ref nil cons cons opType constTerm 2039 def "_1541" 3 ref var 2040 def 2029 ref 1990 ref 2040 ref varTerm 2041 def appTerm 2030 ref appTerm absTerm absTerm 78 ref appTerm 2042 def appTerm refl 2040 ref 2029 ref 2033 remove 2041 ref appTerm 2030 ref appTerm absTerm absTerm 2043 def 2035 ref appTerm betaConv appThm 2039 remove refl 2042 remove betaConv appThm 2037 remove refl appThm trans 12 ref 0 ref 1977 ref 0 ref 1977 remove 8 ref cons opType nil cons cons opType constTerm 2044 def "_1540" 2 ref var 2045 def 2040 remove 2029 remove 1989 ref 2045 remove varTerm appTerm 2041 remove appTerm 2030 remove appTerm absTerm absTerm absTerm 2046 def 76 ref appTerm 2047 def appTerm refl 2046 ref 2032 remove appTerm betaConv appThm 2044 remove refl 2047 remove betaConv appThm 2043 remove refl appThm trans 2046 remove refl nil 1856 ref 1987 ref nil cons cons nil cons nil cons cons 2048 def 1931 remove subst appThm eqMp 202 ref 78 ref appTerm refl 2049 def 202 ref "_1426" 1411 ref var 2050 def 1892 remove 2050 remove varTerm appTerm absTerm 2051 def 1987 ref appTerm 2052 def appTerm refl 2051 remove 2034 ref appTerm betaConv appThm 1935 ref 2052 remove betaConv appThm 2035 remove refl appThm trans 1936 remove 2048 remove 1937 remove subst 2053 def appThm eqMp appThm nil 1565 ref 1986 ref nil cons 2054 def cons 1566 ref 198 remove cons nil cons 2055 def cons nil cons cons 2056 def 1942 remove subst eqMp appThm eqMp 1209 ref 1986 ref appTerm refl 2057 def 1209 ref "_1428" 1411 remove var 2058 def 1898 remove 2058 remove varTerm appTerm absTerm 2059 def 1987 remove appTerm 2060 def appTerm refl 2059 remove 2034 remove appTerm betaConv appThm 1240 ref 2060 remove betaConv appThm 2038 remove refl appThm trans 1946 remove 2053 remove appThm eqMp appThm 2056 remove 1947 remove subst eqMp appThm eqMp sym trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp "A" 1982 remove cons nil cons 2061 def "P" 1847 ref var 2008 ref nil cons 2062 def cons "x" 1846 remove var 2022 remove nil cons cons nil cons cons nil cons cons 1259 ref subst proveHyp nil 90 ref 68 ref 0 ref 1847 ref 8 ref cons opType constTerm 2008 remove appTerm nil cons cons 91 ref 2018 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp nil "p" 1847 ref var 2062 remove cons nil cons nil cons cons 2061 remove 35 ref cons 1328 ref subst subst eqMp eqMp nil 90 ref 43 ref 2016 ref appTerm nil cons cons 91 ref 2017 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 195 ref 44 ref 2016 remove nil cons cons 196 ref cons nil cons cons 162 ref subst eqMp eqMp nil 90 ref 2015 remove nil cons cons 91 ref 2014 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 172 ref 168 ref 2013 remove nil cons cons 199 ref cons nil cons cons 162 ref subst eqMp eqMp nil 90 ref 2012 remove nil cons cons 91 ref 2011 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 1245 ref 1906 ref 2010 remove nil cons cons 1243 ref 2054 ref cons nil cons 2063 def cons nil cons cons 162 ref subst eqMp eqMp subst 2064 def appThm 2000 remove 1870 remove appTerm betaConv appThm nil 61 ref 1990 remove 1864 ref appTerm 1865 remove appTerm 2065 def nil cons cons nil cons nil cons cons 1766 remove subst trans absThm appThm absThm appThm trans absThm appThm trans eqMp eqMp absThm eqMp nil 40 ref 0 ref 1979 remove 8 ref cons opType constTerm 2066 def 1997 remove appTerm thm nil 1980 remove 1981 ref 39 ref 68 ref 1847 remove constTerm 1993 remove appTerm 2067 def appTerm 69 remove 70 ref 73 ref 74 ref 68 ref 1822 remove constTerm 2068 def 1994 remove appTerm absTerm appTerm absTerm 2069 def appTerm 2070 def appTerm 2071 def absTerm 2072 def nil cons cons nil cons nil cons cons 1998 remove subst 1981 remove nil 61 ref 2071 remove nil cons 2073 def cons nil cons nil cons cons 67 ref subst 132 ref nil 1860 ref 2001 remove cons nil cons nil cons cons 1999 remove 1775 ref subst subst 132 ref 1849 ref 1850 ref 1850 ref 275 ref 2002 remove appTerm absTerm 2074 def 1851 ref appTerm betaConv absThm appThm appThm 313 ref 70 ref 1855 ref 1856 ref 2074 ref 1859 ref appTerm betaConv absThm appThm absThm appThm appThm nil 1860 ref 2074 remove nil cons cons nil cons nil cons cons 1861 ref subst eqMp trans 313 ref 70 ref 132 ref 1855 ref 1856 ref 1856 ref 275 ref 2004 remove appTerm absTerm 2075 def 1858 ref appTerm betaConv absThm appThm appThm 490 ref 1566 ref 1863 ref 1565 ref 2075 ref 1866 ref appTerm betaConv absThm appThm absThm appThm appThm nil 1867 ref 2075 remove nil cons cons nil cons nil cons cons 1868 ref subst eqMp 490 ref 1566 ref 1863 ref 1565 ref 312 ref 2064 remove appThm absThm appThm absThm appThm trans absThm appThm trans appThm nil 47 remove 2069 ref nil cons cons nil cons nil cons cons 1775 ref subst 313 ref 49 ref 312 ref 2069 remove 156 ref appTerm betaConv appThm nil 574 remove 74 ref 2068 remove 1985 ref 1989 remove 156 remove appTerm 2076 def 78 ref appTerm 1986 ref appTerm absTerm appTerm absTerm 2077 def nil cons cons nil cons nil cons cons 1780 remove subst 490 ref 197 ref 312 ref 2077 remove 211 ref appTerm betaConv appThm nil "p" 1207 remove var 1985 ref 2076 remove 211 ref appTerm 1986 ref appTerm absTerm 2078 def nil cons cons nil cons nil cons cons 1246 remove 1775 remove subst subst 1863 ref 1243 ref 312 remove 2078 remove 1243 remove varTerm appTerm betaConv appThm absThm appThm trans trans absThm appThm trans trans absThm appThm trans appThm nil 253 remove 43 ref 70 ref 189 ref 1566 ref 1823 ref 1565 ref 275 ref 2065 remove appTerm absTerm appTerm absTerm appTerm absTerm appTerm nil cons cons nil cons nil cons cons 295 remove subst trans sym 66 remove eqMp nil 90 ref 39 ref 275 ref 2067 ref appTerm appTerm 275 ref 2070 ref appTerm appTerm nil cons cons 91 ref 2073 remove cons nil cons cons nil cons cons 152 ref subst proveHyp nil 91 ref 2070 remove nil cons cons 90 ref 2067 remove nil cons cons nil cons cons nil cons cons 1801 remove subst eqMp eqMp absThm eqMp nil 2066 remove 2072 remove appTerm thm nil 1720 ref 1389 ref 260 remove 578 ref 92 ref 98 ref 1769 ref appTerm 43 ref 70 ref 189 ref 74 ref 92 ref 1724 remove appTerm 578 ref varTerm 2079 def 79 remove appTerm appTerm absTerm 2080 def appTerm 2081 def absTerm 2082 def appTerm 2083 def appTerm 2084 def appTerm 2079 ref 1809 remove appTerm 2085 def appTerm 2086 def absTerm 2087 def appTerm 2088 def absTerm 2089 def nil cons cons nil cons nil cons cons 1730 ref subst 1389 ref nil 61 ref 2088 remove nil cons cons nil cons nil cons cons 67 ref subst nil 308 remove 2087 remove nil cons cons nil cons nil cons cons 600 remove subst 578 remove nil 61 ref 2086 remove nil cons cons nil cons nil cons cons 67 ref subst nil 90 ref 2084 remove nil cons 2090 def cons 91 ref 2085 ref nil cons 2091 def cons nil cons 2092 def cons nil cons cons 2093 def 109 ref subst 2093 remove 160 ref subst nil 128 ref 1785 ref cons 130 ref 2083 remove nil cons 2094 def cons nil cons cons nil cons cons 2095 def 144 ref subst 2095 remove 638 remove subst nil 90 ref 1785 remove cons 2096 def 2092 ref cons nil cons cons 152 ref subst nil 44 ref "a0" 2 ref var 2097 def 92 ref 1768 remove 2097 ref varTerm 2098 def appTerm 2099 def appTerm 2085 ref appTerm 2100 def absTerm nil cons cons nil cons nil cons cons 59 ref subst 2097 remove nil 61 ref 2100 remove nil cons cons nil cons nil cons cons 67 ref subst nil 90 ref 2099 ref nil cons 2101 def cons 2092 ref cons nil cons cons 2102 def 109 ref subst 2102 remove 160 ref subst 2099 ref betaConv 2099 remove assume eqMp nil 90 ref 73 remove 74 ref 1391 ref 2098 ref appTerm 2103 def 78 ref appTerm absTerm 2104 def appTerm 2105 def nil cons cons 2092 ref cons nil cons cons 152 ref subst proveHyp nil 168 ref "b0" 3 ref var 2106 def 92 ref 2104 ref 2106 ref varTerm 2107 def appTerm 2108 def appTerm 2085 ref appTerm 2109 def absTerm nil cons cons nil cons nil cons cons 174 ref subst 2106 remove nil 61 ref 2109 remove nil cons cons nil cons nil cons cons 67 ref subst nil 90 ref 2108 ref nil cons 2110 def cons 2092 ref cons nil cons cons 2111 def 109 ref subst 2111 remove 160 ref subst 2108 ref betaConv 2108 remove assume eqMp nil 90 ref 2103 remove 2107 ref appTerm nil cons 2112 def cons 2113 def 2092 remove cons nil cons cons 2114 def 152 ref subst proveHyp 2114 ref 109 ref subst 2114 remove 160 ref subst 1805 remove 39 remove "_1580" 9 remove var 2115 def 2079 ref 1802 remove 2115 remove varTerm appTerm appTerm absTerm 2116 def 1725 ref appTerm 2117 def appTerm refl 2116 ref 1807 ref appTerm betaConv appThm 132 ref 2117 remove betaConv appThm 2079 ref 1808 ref appTerm 2118 def refl appThm trans 2116 remove refl 1731 remove 1725 remove appTerm 1807 ref appTerm assume appThm eqMp sym nil "P" 0 ref 0 ref 1385 ref 16 remove cons opType 2119 def 8 ref cons opType 2120 def var 2121 def "c" 2119 ref var 2122 def 92 ref 1387 ref 1389 ref 88 ref 11 ref 92 ref 1806 ref appTerm 2123 def 1391 ref 21 ref 2122 ref varTerm 1391 ref appTerm 2124 def appTerm 2125 def appTerm 26 ref 2124 ref appTerm 2126 def appTerm 2127 def appTerm absTerm 2128 def appTerm 2129 def absTerm 2130 def appTerm 2131 def appTerm 2132 def 2079 ref 2124 ref appTerm 2133 def appTerm 2134 def absTerm nil cons cons nil cons nil cons cons "A" 2119 ref nil cons cons nil cons 2135 def 35 ref cons 59 ref subst subst 2122 remove nil 61 ref 2134 remove nil cons cons nil cons nil cons cons 67 ref subst nil 90 ref 2131 remove nil cons 2136 def cons 2137 def 91 ref 2133 remove nil cons 2138 def cons nil cons cons nil cons cons 2139 def 109 ref subst 2139 remove 160 ref subst 2079 ref refl 2140 def nil 11 ref 2124 remove nil cons cons nil cons nil cons cons 1054 remove subst appThm sym 1410 remove sym nil 2096 remove nil cons nil cons cons 296 remove subst sym nil 90 ref 1784 ref nil cons 2141 def cons 300 ref cons nil cons cons 2142 def 109 ref subst 2142 remove 160 ref subst nil 2113 remove 300 remove cons nil cons cons 152 ref subst nil "_1586" 3 ref var 2143 def 2107 remove nil cons cons "_1585" 2 ref var 2144 def 2098 remove nil cons cons nil cons cons nil cons cons nil 90 ref 1391 ref 2144 remove varTerm 2145 def appTerm 2146 def 2143 remove varTerm 2147 def appTerm nil cons cons nil cons nil cons cons 831 remove subst 74 ref 275 remove 2146 remove 78 ref appTerm appTerm absTerm 2148 def 2147 ref appTerm 2149 def betaConv 1782 ref 2145 ref appTerm 2150 def betaConv 1781 remove 1784 remove assume eqMp nil 90 ref 1783 remove cons 91 ref 2150 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 195 ref 44 ref 1782 remove nil cons cons 49 ref 2145 remove nil cons cons nil cons cons nil cons cons 162 ref subst eqMp eqMp nil 90 ref 189 ref 2148 ref appTerm nil cons cons 91 ref 2149 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 172 ref 168 ref 2148 remove nil cons cons 197 ref 2147 remove nil cons cons nil cons cons nil cons cons 162 ref subst eqMp eqMp eqMp subst eqMp eqMp nil 128 ref 2141 remove cons 832 remove cons nil cons cons 144 ref subst deductAntisym eqMp eqMp eqMp nil 90 ref 487 remove 1807 ref appTerm 2151 def nil cons 2152 def cons 2153 def 91 ref 2127 ref nil cons 2154 def cons nil cons 2155 def cons nil cons cons 2156 def 152 ref subst proveHyp 2156 ref 109 ref subst 2156 remove 160 ref subst nil 2137 ref 2155 ref cons nil cons cons 2157 def 152 ref subst nil 2153 remove 91 ref 2132 remove 2127 remove appTerm 2158 def nil cons 2159 def cons nil cons 2160 def cons nil cons cons 152 ref subst nil 10 ref 11 ref 92 ref 1807 ref 22 ref appTerm 2161 def appTerm 2158 ref appTerm 2162 def absTerm 2163 def nil cons cons nil cons nil cons cons 60 remove subst 11 ref nil 61 ref 2162 remove nil cons cons nil cons nil cons cons 67 ref subst nil 90 ref 2161 ref nil cons 2164 def cons 2160 ref cons nil cons cons 2165 def 109 ref subst 2165 remove 160 ref subst 2161 ref betaConv 2166 def 2161 remove assume eqMp nil 90 ref 1806 remove nil cons 2167 def cons 2168 def 2160 remove cons nil cons cons 2169 def 152 ref subst proveHyp 2169 ref 109 ref subst 2169 remove 160 ref subst 2157 ref 109 ref subst 2157 remove 160 ref subst nil 2168 remove 2155 remove cons nil cons cons 152 ref subst 2128 ref 22 remove appTerm 2170 def betaConv 2130 ref 1391 ref appTerm 2171 def betaConv nil 2137 remove 91 ref 2171 remove nil cons cons nil cons cons nil cons cons 152 ref subst 1405 remove 1720 ref 2130 remove nil cons cons "x" 1385 remove var 1803 remove cons nil cons cons nil cons cons 162 ref subst eqMp eqMp nil 90 ref 2129 remove nil cons cons 91 ref 2170 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 34 ref 10 ref 2128 remove nil cons cons 154 remove cons nil cons cons 162 ref subst eqMp eqMp eqMp eqMp nil 128 ref 2136 remove cons 2172 def 130 ref 2154 ref cons nil cons 2173 def cons nil cons cons 144 ref subst deductAntisym eqMp eqMp nil 128 ref 2167 remove cons 130 ref 2159 remove cons nil cons 2174 def cons nil cons cons 144 ref subst deductAntisym eqMp eqMp eqMp nil 128 ref 2164 remove cons 2174 ref cons nil cons cons 144 ref subst deductAntisym eqMp eqMp absThm eqMp nil 90 ref 88 ref 2163 remove appTerm nil cons cons 91 ref 92 ref 2151 remove appTerm 2158 remove appTerm nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 34 ref 10 remove 1807 ref nil cons cons 2175 def 2174 remove cons nil cons cons 256 ref subst eqMp eqMp eqMp eqMp nil 128 ref 2152 remove cons 2173 remove cons nil cons cons 144 ref subst deductAntisym eqMp eqMp nil 90 ref 2154 remove cons 91 ref 2079 ref 17 remove 2125 ref appTerm 2126 ref appTerm appTerm nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp nil 74 ref 2126 remove nil cons cons 70 ref 2125 remove nil cons cons nil cons cons nil cons cons 2080 ref 78 ref appTerm 2176 def betaConv 2082 ref 76 ref appTerm 2177 def betaConv nil 90 ref 2094 remove cons 91 ref 2177 remove nil cons cons nil cons cons nil cons cons 152 ref subst 195 ref 44 ref 2082 remove nil cons cons 196 ref cons nil cons cons 162 ref subst eqMp eqMp nil 90 ref 2081 remove nil cons cons 91 ref 2176 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 172 ref 168 ref 2080 remove nil cons cons 199 ref cons nil cons cons 162 ref subst eqMp eqMp subst eqMp eqMp eqMp nil 2172 remove 130 ref 2138 remove cons nil cons cons nil cons cons 144 ref subst deductAntisym eqMp eqMp absThm eqMp nil 90 ref 40 ref 0 ref 2120 ref 8 ref cons opType constTerm "_1584" 2119 ref var 2178 def 92 ref 1387 ref 1389 ref 88 ref 11 ref 2123 ref 1391 ref 21 ref 2178 ref varTerm 2179 def 1391 ref appTerm 2180 def appTerm appTerm 26 ref 2180 ref appTerm appTerm appTerm absTerm appTerm absTerm appTerm appTerm 2079 remove 2180 ref appTerm appTerm absTerm 2181 def appTerm 2182 def nil cons 2183 def cons 2184 def 91 ref 2118 ref nil cons 2185 def cons nil cons 2186 def cons nil cons cons 152 ref subst proveHyp 1389 ref 1808 ref absTerm 2187 def refl nil 90 ref 12 ref 0 ref 2119 ref 2120 remove nil cons cons opType constTerm 2188 def 2187 ref appTerm 2187 ref appTerm nil cons cons 91 ref 92 ref 2182 remove appTerm 2189 def 2118 ref appTerm 2190 def nil cons 2191 def cons nil cons 2192 def cons nil cons cons 152 ref subst proveHyp nil 2178 remove 2187 ref nil cons cons nil cons nil cons cons nil 90 ref 2188 remove 2179 ref appTerm 2187 ref appTerm 2193 def nil cons 2194 def cons 2192 ref cons nil cons cons 2195 def 109 ref subst 2195 remove 160 ref subst nil 90 ref 92 ref 1387 ref 1389 ref 88 remove 11 ref 2123 ref 1391 ref 21 ref 1808 ref appTerm appTerm 26 ref 1808 ref appTerm appTerm appTerm absTerm appTerm 2196 def absTerm 2197 def appTerm 2198 def appTerm 2118 ref appTerm 2199 def nil cons 2200 def cons 2186 ref cons nil cons cons 2201 def 109 ref subst 2201 remove 160 ref subst nil 1720 remove 2197 remove nil cons cons nil cons nil cons cons 1730 remove subst 1389 ref nil 61 ref 2196 remove nil cons cons nil cons nil cons cons 67 ref subst 471 ref 11 ref 713 ref 2166 remove appThm 1807 remove 1808 remove appTerm betaConv appThm absThm appThm 34 remove 2175 remove nil cons nil cons cons 1312 remove 45 remove appTerm 2202 def betaConv 1315 remove nil 1316 remove 91 ref 2202 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 351 remove 1317 remove 353 remove 315 remove cons nil cons cons nil cons cons 162 ref subst eqMp eqMp subst eqMp eqMp absThm eqMp nil 90 ref 2198 remove nil cons cons 2186 remove cons nil cons cons 152 ref subst proveHyp 2199 ref assume eqMp eqMp nil 128 ref 2200 ref cons 130 ref 2185 ref cons nil cons cons nil cons cons 144 ref subst deductAntisym eqMp nil 90 ref 92 ref 2199 ref appTerm 2118 remove appTerm 2203 def nil cons cons 2192 remove cons nil cons cons 152 ref subst proveHyp nil 2184 ref 91 ref 2200 ref cons 2204 def nil cons cons nil cons cons 2205 def 109 ref subst 2205 remove 160 ref subst 713 remove 1388 remove 1389 remove 471 remove 11 remove 2123 remove refl 1403 ref 21 remove refl 14 remove 2180 remove appTerm refl 2187 remove 1391 remove appTerm betaConv appThm 2193 remove assume 1403 remove appThm eqMp sym 2206 def appThm appThm 26 remove refl 2206 ref appThm appThm appThm absThm appThm absThm appThm appThm 2140 remove 2206 remove appThm appThm sym 2181 ref 2179 ref appTerm 2207 def betaConv nil 2184 ref 91 ref 2207 remove nil cons cons nil cons cons nil cons cons 152 ref subst 2135 remove 2121 remove 2181 remove nil cons cons "x" 2119 remove var 2179 remove nil cons cons nil cons cons nil cons cons 162 ref subst eqMp eqMp eqMp eqMp nil 128 ref 2183 remove cons 130 ref 2200 remove cons nil cons cons nil cons cons 144 ref subst deductAntisym eqMp nil 90 ref 2189 remove 2199 remove appTerm nil cons cons 91 ref 92 ref 2203 remove appTerm 2190 remove appTerm nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp nil 2184 remove 2204 remove 456 remove 2185 remove cons nil cons cons cons nil cons cons nil 975 remove 91 ref 465 remove 467 ref appTerm nil cons 2208 def cons nil cons cons nil cons cons 2209 def 109 ref subst 2209 remove 160 ref subst nil 90 ref 464 ref nil cons 2210 def cons 91 ref 467 remove nil cons 2211 def cons nil cons cons nil cons cons 2212 def 109 ref subst 2212 remove 160 ref subst nil 1154 remove 91 ref 738 ref cons nil cons 2213 def cons nil cons cons 2214 def 109 remove subst 2214 remove 160 ref subst 151 remove nil 978 remove 2213 remove cons nil cons cons 152 ref subst proveHyp 464 remove assume eqMp eqMp nil 129 remove 130 ref 738 remove cons nil cons cons nil cons cons 144 ref subst deductAntisym eqMp eqMp nil 128 ref 2210 remove cons 130 ref 2211 remove cons nil cons cons nil cons cons 144 ref subst deductAntisym eqMp eqMp nil 983 remove 130 ref 2208 remove cons nil cons cons nil cons cons 144 ref subst deductAntisym eqMp subst eqMp eqMp eqMp nil 128 ref 2194 remove cons 130 ref 2191 remove cons nil cons cons nil cons cons 144 ref subst deductAntisym eqMp subst eqMp eqMp eqMp proveHyp eqMp nil 128 ref 2112 remove cons 130 remove 2091 remove cons nil cons 2215 def cons nil cons cons 144 ref subst deductAntisym eqMp eqMp eqMp nil 128 ref 2110 remove cons 2215 ref cons nil cons cons 144 ref subst deductAntisym eqMp eqMp absThm eqMp nil 90 ref 189 ref 197 remove 92 ref 2104 ref 211 remove appTerm appTerm 2085 ref appTerm absTerm appTerm nil cons cons 91 ref 92 ref 2105 remove appTerm 2085 ref appTerm nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 172 ref 168 ref 2104 remove nil cons cons 2215 ref cons nil cons cons 256 ref subst eqMp eqMp eqMp nil 128 ref 2101 remove cons 2215 ref cons nil cons cons 144 ref subst deductAntisym eqMp eqMp absThm eqMp nil 90 ref 43 ref 49 remove 92 ref 1778 remove appTerm 2085 ref appTerm absTerm appTerm nil cons cons 91 ref 92 remove 1769 remove appTerm 2085 remove appTerm nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 195 ref 44 ref 1777 remove cons 2215 ref cons nil cons cons 256 remove subst eqMp eqMp proveHyp proveHyp eqMp nil 128 remove 2090 remove cons 2215 remove cons nil cons cons 144 remove subst deductAntisym eqMp eqMp absThm eqMp eqMp absThm eqMp nil 1387 remove 2089 remove appTerm thm nil 1214 remove 1077 ref 1687 remove 1579 remove appTerm 1078 remove appTerm absTerm 2216 def nil cons cons nil cons nil cons cons 1664 remove subst 1077 remove 1715 remove absThm eqMp nil 90 ref 1076 remove 2216 remove appTerm 2217 def nil cons cons 91 ref 98 ref 1816 remove 1817 ref 1961 remove 1820 remove 1821 remove 43 ref 70 ref 189 ref 74 ref 1823 ref 1985 ref 1826 ref 1827 remove 1988 ref appTerm appTerm 1836 ref 1988 remove appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 2218 def appTerm 1836 ref appTerm absTerm 2219 def appTerm 2220 def appTerm 40 ref 0 ref 0 ref 0 ref 1 ref 2 ref 1 ref 3 ref 1 remove 1918 remove opType 2221 def nil cons 2222 def cons opType 2223 def nil cons 2224 def cons opType 2225 def "E" varType 2226 def nil cons 2227 def cons opType 2228 def 8 ref cons opType 2229 def 8 ref cons opType 2230 def constTerm "f" 2228 ref var 2231 def 12 ref 0 ref 2228 ref 2229 ref nil cons cons opType constTerm 1205 ref 0 ref 2229 ref 2228 ref nil cons 2232 def cons opType constTerm 2233 def "f'" 2228 ref var 2234 def 43 ref 70 ref 189 ref 74 ref 1823 ref 1985 ref 40 ref 0 ref 1825 ref 8 ref cons opType constTerm 2235 def "d" 1811 ref var 2236 def 12 ref 0 ref 2226 ref 0 ref 2226 ref 8 ref cons opType nil cons cons opType constTerm 2237 def 2234 remove varTerm 15 ref 0 ref 2 ref 0 ref 2223 ref 2225 ref nil cons 2238 def cons opType nil cons cons opType constTerm 2239 def 76 ref appTerm 2240 def 15 ref 0 ref 3 ref 0 ref 2221 ref 2224 ref cons opType nil cons cons opType constTerm 2241 def 78 ref appTerm 2242 def 15 remove 0 ref 1055 ref 0 ref 1811 ref 2222 ref cons opType nil cons cons opType constTerm 2243 def 1986 ref appTerm 2244 def 2236 ref varTerm 2245 def appTerm 2246 def appTerm 2247 def appTerm 2248 def appTerm appTerm 2231 ref varTerm 2249 def 2248 ref appTerm 2250 def appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 2251 def appTerm 2249 ref appTerm absTerm 2252 def appTerm 2253 def appTerm 2254 def nil cons cons nil cons cons nil cons cons 160 ref subst proveHyp nil 1949 remove 2219 remove nil cons cons nil cons nil cons cons 1952 remove 59 ref subst subst 1817 ref nil 1818 remove 1975 remove cons 1817 remove 2218 ref nil cons cons nil cons cons nil cons cons 1845 remove subst 132 ref 1849 remove 1850 ref 1850 remove 1826 ref 2218 ref 1851 ref appTerm appTerm 1836 ref 1851 ref appTerm appTerm absTerm 2255 def 1851 remove appTerm betaConv absThm appThm appThm 313 ref 70 ref 1855 ref 1856 ref 2255 ref 1859 ref appTerm betaConv absThm appThm absThm appThm appThm nil 1860 remove 2255 remove nil cons cons nil cons nil cons cons 1861 remove subst eqMp trans 313 ref 70 ref 132 ref 1855 remove 1856 ref 1856 remove 1826 ref 2218 remove 1859 ref appTerm appTerm 1836 remove 1859 remove appTerm appTerm absTerm 2256 def 1858 remove appTerm betaConv absThm appThm appThm 490 ref 1566 ref 1863 ref 1565 ref 2256 ref 1866 remove appTerm betaConv absThm appThm absThm appThm appThm nil 1867 remove 2256 remove nil cons cons nil cons nil cons cons 1868 remove subst eqMp 490 ref 1566 ref 1863 ref 1565 remove 1869 ref 1953 remove appThm 1955 remove refl appThm 1958 remove trans absThm appThm 1959 ref trans absThm appThm 1248 ref trans trans absThm appThm 1249 ref trans trans absThm eqMp nil 90 ref 2220 remove nil cons cons 91 ref 2253 remove nil cons cons nil cons cons nil cons cons 160 remove subst proveHyp nil "P" 2229 ref var 2257 def 2252 remove nil cons cons nil cons nil cons cons "A" 2232 remove cons nil cons 2258 def 35 ref cons 2259 def 59 ref subst subst 2231 ref nil "g" 2228 ref var 2249 ref nil cons cons 2231 remove 2251 ref nil cons cons nil cons cons nil cons cons "A" 2238 remove cons "B" 2227 ref cons nil cons cons 35 ref cons 1596 remove subst subst 132 ref 40 ref 0 ref 0 ref 2225 ref 8 ref cons opType 2260 def 8 ref cons opType constTerm refl "x" 2225 ref var 2261 def 2261 ref 2237 ref 2251 ref 2261 remove varTerm 2262 def appTerm appTerm 2249 ref 2262 ref appTerm appTerm absTerm 2263 def 2262 remove appTerm betaConv absThm appThm appThm 313 ref 70 ref 40 ref 0 ref 0 ref 2223 ref 8 ref cons opType 2264 def 8 ref cons opType constTerm 2265 def refl 2266 def "b" 2223 ref var 2267 def 2263 ref 2240 ref 2267 ref varTerm 2268 def appTerm 2269 def appTerm betaConv absThm appThm absThm appThm appThm nil "p" 2260 remove var 2263 remove nil cons cons nil cons nil cons cons 194 remove "B" 2224 ref cons nil cons cons 35 ref cons 2270 def 1402 ref subst subst eqMp trans 313 remove 70 ref 132 ref 2266 remove 2267 ref 2267 ref 2237 ref 2251 ref 2269 ref appTerm appTerm 2249 ref 2269 ref appTerm appTerm absTerm 2271 def 2268 ref appTerm betaConv absThm appThm appThm 490 ref 1566 ref 40 remove 0 ref 0 ref 2221 ref 8 ref cons opType 2272 def 8 ref cons opType constTerm 2273 def refl 2274 def "b" 2221 ref var 2275 def 2271 ref 2241 ref 1864 ref appTerm 2276 def 2275 ref varTerm 2277 def appTerm 2278 def appTerm betaConv absThm appThm absThm appThm appThm nil "p" 2264 ref var 2271 remove nil cons cons nil cons nil cons cons 171 remove "B" 2222 ref cons nil cons cons 35 ref cons 2279 def 1402 ref subst subst eqMp 490 remove 1566 ref 132 remove 2274 remove 2275 ref 2275 ref 2237 ref 2251 remove 2240 ref 2278 ref appTerm 2280 def appTerm appTerm 2249 ref 2280 remove appTerm appTerm absTerm 2281 def 2277 ref appTerm betaConv absThm appThm appThm 1863 ref "a" 1055 ref var 2282 def 2235 ref refl 2283 def "b" 1811 ref var 2284 def 2281 ref 2243 ref 2282 ref varTerm 2285 def appTerm 2284 ref varTerm 2286 def appTerm 2287 def appTerm betaConv absThm appThm absThm appThm appThm nil "p" 2272 ref var 2281 remove nil cons cons nil cons nil cons cons 1244 remove 1844 remove cons 35 ref cons 2288 def 1402 remove subst subst eqMp 1863 remove 2282 ref 2283 remove 2284 ref 2237 ref refl 2289 def nil 2236 ref 2286 ref nil cons cons 1985 ref 2285 ref nil cons cons 2006 remove cons cons nil cons cons 2236 ref 2237 ref 2233 remove "_1468" 2228 ref var 2290 def 43 ref 70 ref 189 ref 74 ref 1823 ref 1985 ref 2235 ref 2236 ref 2237 ref 2290 remove varTerm 2248 ref appTerm appTerm 2250 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 2291 def appTerm 2292 def 2248 ref appTerm appTerm 2250 ref appTerm absTerm 2293 def 2245 ref appTerm 2294 def betaConv 1985 ref 2235 ref 2293 ref appTerm 2295 def absTerm 2296 def 1986 ref appTerm 2297 def betaConv 74 ref 1823 ref 2296 ref appTerm 2298 def absTerm 2299 def 78 ref appTerm 2300 def betaConv 70 ref 189 ref 2299 ref appTerm 2301 def absTerm 2302 def 76 ref appTerm 2303 def betaConv 2291 ref 2292 remove appTerm 2304 def betaConv 2291 ref "_1466" 2225 ref var 2305 def 2249 ref 2239 ref 1205 ref 0 ref 0 ref 0 ref 2225 ref 19 remove cons opType 2306 def 8 ref cons opType 2306 ref nil cons cons opType constTerm "fn" 2306 remove var 2307 def 43 ref 70 ref 2265 ref 2267 ref 186 remove 2307 remove varTerm 2269 ref appTerm appTerm 76 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm 2308 def 2305 remove varTerm 2309 def appTerm appTerm 2241 ref 1205 ref 0 ref 0 ref 0 ref 2223 ref 4 remove cons opType 2310 def 8 ref cons opType 2310 ref nil cons cons opType constTerm "fn" 2310 remove var 2311 def 189 ref 1566 ref 2273 ref 2275 ref 202 ref 2311 remove varTerm 2278 ref appTerm appTerm 1864 remove appTerm absTerm appTerm absTerm appTerm absTerm appTerm 2312 def 1205 ref 0 ref 0 ref 0 ref 2225 remove 2224 remove cons opType 2313 def 8 ref cons opType 2313 ref nil cons cons opType constTerm "fn" 2313 remove var 2314 def 43 ref 70 ref 2265 remove 2267 ref 12 ref 0 ref 2223 ref 2264 remove nil cons cons opType constTerm 2314 remove varTerm 2269 remove appTerm appTerm 2268 remove appTerm absTerm appTerm absTerm appTerm absTerm appTerm 2315 def 2309 remove appTerm 2316 def appTerm appTerm 2243 ref 1205 ref 0 ref 0 ref 0 ref 2221 ref 1056 remove cons opType 2317 def 8 ref cons opType 2317 ref nil cons cons opType constTerm "fn" 2317 remove var 2318 def 1823 ref 2282 ref 2235 ref 2284 ref 1209 ref 2318 remove varTerm 2287 ref appTerm appTerm 2285 remove appTerm absTerm appTerm absTerm appTerm absTerm appTerm 2319 def 1205 ref 0 ref 0 ref 0 ref 2223 ref 2222 remove cons opType 2320 def 8 ref cons opType 2320 ref nil cons cons opType constTerm "fn" 2320 remove var 2321 def 189 ref 1566 remove 2273 remove 2275 ref 12 ref 0 ref 2221 ref 2272 remove nil cons cons opType constTerm 2321 remove varTerm 2278 remove appTerm appTerm 2277 remove appTerm absTerm appTerm absTerm appTerm absTerm appTerm 2322 def 2316 remove appTerm 2323 def appTerm appTerm 1205 remove 0 ref 0 ref 0 ref 2221 ref 1812 remove cons opType 2324 def 8 ref cons opType 2324 ref nil cons cons opType constTerm "fn" 2324 remove var 2325 def 1823 ref 2282 ref 2235 ref 2284 ref 1826 ref 2325 remove varTerm 2287 ref appTerm appTerm 2286 remove appTerm absTerm appTerm absTerm appTerm absTerm appTerm 2326 def 2323 remove appTerm appTerm appTerm appTerm appTerm absTerm 2327 def appTerm betaConv sym nil 44 ref 70 ref 189 remove 74 ref 1823 remove 1985 ref 2235 remove 2236 ref 2237 ref 2327 ref 2248 ref appTerm 2328 def appTerm 2250 remove appTerm 2329 def absTerm 2330 def appTerm 2331 def absTerm 2332 def appTerm 2333 def absTerm 2334 def appTerm 2335 def absTerm nil cons cons nil cons nil cons cons 59 ref subst 70 remove nil 61 ref 2335 remove nil cons cons nil cons nil cons cons 67 ref subst nil 168 ref 2334 remove nil cons cons nil cons nil cons cons 174 remove subst 74 remove nil 61 ref 2333 remove nil cons cons nil cons nil cons cons 67 ref subst nil 1906 ref 2332 remove nil cons cons nil cons nil cons cons 1907 remove subst 1985 remove nil 61 ref 2331 remove nil cons cons nil cons nil cons cons 67 ref subst nil "P" 1825 remove var 2336 def 2330 remove nil cons cons nil cons nil cons cons 1957 ref 59 remove subst subst 2236 remove nil 61 remove 2329 remove nil cons cons nil cons nil cons cons 67 remove subst 2328 remove betaConv 2237 remove "_1461" 1811 ref var 2337 def 2249 ref 2240 ref 2242 ref 2244 remove 2337 ref varTerm 2338 def appTerm appTerm appTerm appTerm absTerm 2245 ref appTerm 2339 def appTerm refl 2337 ref 2249 ref 2239 ref 2308 remove 2248 ref appTerm 2340 def appTerm 2341 def 2241 ref 2312 ref 2315 remove 2248 remove appTerm 2342 def appTerm 2343 def appTerm 2344 def 2243 ref 2319 ref 2322 ref 2342 ref appTerm 2345 def appTerm 2346 def appTerm 2347 def 2338 ref appTerm appTerm appTerm appTerm absTerm 2348 def 2326 ref 2345 remove appTerm 2349 def appTerm betaConv appThm 2289 remove 2339 remove betaConv appThm 2249 ref 2341 ref 2344 ref 2347 remove 2349 ref appTerm appTerm appTerm appTerm refl appThm trans 12 ref 0 ref 0 ref 1811 remove 2227 ref cons opType 2350 def 0 ref 2350 ref 8 ref cons opType nil cons cons opType constTerm 2351 def "_1460" 1055 ref var 2352 def 2337 ref 2249 ref 2240 ref 2242 remove 2243 remove 2352 ref varTerm appTerm 2338 remove appTerm 2353 def appTerm appTerm appTerm absTerm absTerm 1986 remove appTerm 2354 def appTerm refl 2352 ref 2337 ref 2249 ref 2341 ref 2344 remove 2353 ref appTerm appTerm appTerm absTerm absTerm 2355 def 2346 ref appTerm betaConv appThm 2351 remove refl 2354 remove betaConv appThm 2348 remove refl appThm trans 12 ref 0 ref 0 ref 1055 remove 2350 remove nil cons cons opType 2356 def 0 ref 2356 ref 8 ref cons opType nil cons cons opType constTerm 2357 def "_1459" 3 ref var 2358 def 2352 ref 2337 ref 2249 ref 2240 ref 2241 remove 2358 ref varTerm appTerm 2353 remove appTerm 2359 def appTerm appTerm absTerm absTerm absTerm 78 remove appTerm 2360 def appTerm refl 2358 ref 2352 ref 2337 ref 2249 ref 2341 remove 2359 ref appTerm appTerm absTerm absTerm absTerm 2361 def 2343 ref appTerm betaConv appThm 2357 remove refl 2360 remove betaConv appThm 2355 remove refl appThm trans 12 remove 0 ref 0 ref 3 remove 2356 remove nil cons cons opType 2362 def 0 remove 2362 remove 8 remove cons opType nil cons cons opType constTerm 2363 def "_1458" 2 remove var 2364 def 2358 remove 2352 remove 2337 remove 2249 ref 2239 remove 2364 remove varTerm appTerm 2359 remove appTerm appTerm absTerm absTerm absTerm absTerm 2365 def 76 remove appTerm 2366 def appTerm refl 2365 ref 2340 remove appTerm betaConv appThm 2363 remove refl 2366 remove betaConv appThm 2361 remove refl appThm trans 2365 remove refl nil 2267 remove 2247 ref nil cons cons nil cons nil cons cons 2367 def 2270 ref 1671 ref subst subst appThm eqMp 2049 remove 202 remove "_1452" 2223 ref var 2368 def 2312 remove 2368 remove varTerm appTerm absTerm 2369 def 2247 ref appTerm 2370 def appTerm refl 2369 ref 2342 ref appTerm betaConv appThm 1935 remove 2370 remove betaConv appThm 2343 remove refl appThm trans 2369 remove refl 2367 remove 2270 remove 1681 ref subst subst 2371 def appThm eqMp appThm nil 2275 remove 2246 ref nil cons cons 2055 remove cons nil cons cons 2372 def 2279 ref 1671 ref subst subst eqMp appThm eqMp 2057 ref 1209 ref "_1454" 2223 ref var 2373 def 2319 ref 2322 ref 2373 remove varTerm appTerm appTerm absTerm 2374 def 2247 ref appTerm 2375 def appTerm refl 2374 ref 2342 ref appTerm betaConv appThm 1240 ref 2375 remove betaConv appThm 2346 remove refl appThm trans 2374 remove refl 2371 ref appThm eqMp appThm 2057 remove 1209 remove "_1448" 2221 ref var 2376 def 2319 ref 2376 remove varTerm appTerm absTerm 2377 def 2246 ref appTerm 2378 def appTerm refl 2377 ref 2322 ref 2247 ref appTerm 2379 def appTerm betaConv appThm 1240 remove 2378 remove betaConv appThm 2319 remove 2379 ref appTerm refl appThm trans 2377 remove refl 2372 remove 2279 remove 1681 ref subst subst 2380 def appThm eqMp appThm nil 2284 remove 2245 ref nil cons 2381 def cons 2282 remove 2054 remove cons nil cons cons nil cons cons 2382 def 2288 ref 1671 remove subst subst eqMp eqMp appThm eqMp 1826 ref 2245 remove appTerm refl 2383 def 1826 ref "_1456" 2223 remove var 2384 def 2326 ref 2322 remove 2384 remove varTerm appTerm appTerm absTerm 2385 def 2247 remove appTerm 2386 def appTerm refl 2385 ref 2342 remove appTerm betaConv appThm 1869 ref 2386 remove betaConv appThm 2349 remove refl appThm trans 2385 remove refl 2371 remove appThm eqMp appThm 2383 remove 1826 remove "_1450" 2221 remove var 2387 def 2326 ref 2387 remove varTerm appTerm absTerm 2388 def 2246 remove appTerm 2389 def appTerm refl 2388 ref 2379 ref appTerm betaConv appThm 1869 remove 2389 remove betaConv appThm 2326 remove 2379 remove appTerm refl appThm trans 2388 remove refl 2380 remove appThm eqMp appThm 2382 remove 2288 remove 1681 remove subst subst eqMp eqMp appThm eqMp sym trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp 2258 remove 2257 remove 2291 ref nil cons 2390 def cons "x" 2228 remove var 2327 remove nil cons cons nil cons cons nil cons cons 1259 remove subst proveHyp nil 90 ref 68 remove 2230 remove constTerm 2291 remove appTerm nil cons cons 91 ref 2304 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp nil "p" 2229 remove var 2390 remove cons nil cons nil cons cons 2259 remove 1328 remove subst subst eqMp eqMp nil 90 ref 43 remove 2302 ref appTerm nil cons cons 91 ref 2303 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 195 remove 44 remove 2302 remove nil cons cons 196 remove cons nil cons cons 162 ref subst eqMp eqMp nil 90 ref 2301 remove nil cons cons 91 ref 2300 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 172 remove 168 remove 2299 remove nil cons cons 199 remove cons nil cons cons 162 ref subst eqMp eqMp nil 90 ref 2298 remove nil cons cons 91 ref 2297 remove nil cons cons nil cons cons nil cons cons 152 ref subst proveHyp 1245 remove 1906 remove 2296 remove nil cons cons 2063 remove cons nil cons cons 162 ref subst eqMp eqMp nil 90 remove 2295 remove nil cons cons 91 remove 2294 remove nil cons cons nil cons cons nil cons cons 152 remove subst proveHyp 1956 remove 2336 remove 2293 remove nil cons cons 1954 remove 2381 remove cons nil cons cons nil cons cons 162 remove subst eqMp eqMp subst appThm 2249 remove 2240 remove 2276 remove 2287 remove appTerm appTerm appTerm 2391 def refl appThm nil "x" 2226 remove var 2391 remove nil cons cons nil cons nil cons cons "A" 2227 remove cons nil cons 35 remove cons 294 remove subst subst trans absThm appThm 705 remove 1957 remove 1111 remove subst subst trans absThm appThm 1959 remove trans trans absThm appThm 1248 remove trans trans absThm appThm 1249 remove trans trans absThm eqMp eqMp eqMp nil 98 remove 2217 remove appTerm 2254 remove appTerm thm