path: "vendor/opentheory/data/theories/gfp-div-gcd-def/gfp-div-gcd-def.art"
6 version "Number.GF(p).divGcd" "f" "->" typeOp 0 def "Number.Natural.natural" typeOp nil opType 1 def 0 ref 1 ref 0 ref "Number.GF(p).gfp" typeOp nil opType 2 def 0 ref 2 ref 2 ref nil cons 3 def cons 4 def opType 5 def nil cons cons opType 6 def nil cons 7 def cons opType 8 def nil cons cons opType 9 def var 10 def nil cons cons nil cons 10 ref "Data.Bool.!" const 11 def 0 ref 0 ref 1 ref "bool" typeOp nil opType 12 def nil cons 13 def cons opType 14 def 13 ref cons opType constTerm 15 def "u" 1 ref var 16 def 15 ref "v" 1 ref var 17 def 11 ref 0 ref 0 ref 2 ref 13 ref cons opType 18 def 13 ref cons opType 19 def constTerm 20 def "x1" 2 ref var 21 def 20 ref "x2" 2 ref var 22 def "=" const 23 def 0 ref 2 ref 18 ref nil cons cons opType 24 def constTerm 25 def 10 remove varTerm 26 def 16 ref varTerm 27 def appTerm 28 def 17 ref varTerm 29 def appTerm 21 ref varTerm 30 def appTerm 22 ref varTerm 31 def appTerm appTerm "Data.Bool.cond" const 32 def 0 ref 12 ref 7 remove cons opType constTerm 33 def 23 ref 0 ref 1 ref 14 ref nil cons cons opType 34 def constTerm 35 def 27 ref appTerm "Number.Natural.bit1" const 0 ref 1 ref 1 ref nil cons 36 def cons opType 37 def constTerm "Number.Natural.zero" const 1 ref constTerm appTerm 38 def appTerm 39 def appTerm 40 def 30 ref appTerm 41 def 33 ref 35 ref 29 ref appTerm 42 def 38 ref appTerm 43 def appTerm 31 ref appTerm 44 def 33 ref "Number.Natural.even" const 14 ref constTerm 45 def 27 ref appTerm 46 def appTerm 47 def 26 ref "Number.Natural.div" const 0 ref 1 ref 37 ref nil cons cons opType 48 def constTerm 49 def 27 ref appTerm "Number.Natural.bit0" const 37 remove constTerm 38 ref appTerm 50 def appTerm 51 def appTerm 29 ref appTerm "Number.GF(p)./" const 6 ref constTerm 52 def 30 ref appTerm "Number.GF(p).fromNatural" const 0 ref 1 ref 3 ref cons opType constTerm 50 ref appTerm 53 def appTerm 54 def appTerm 31 ref appTerm appTerm 33 ref 45 ref 29 ref appTerm 55 def appTerm 56 def 28 ref 49 ref 29 ref appTerm 50 ref appTerm 57 def appTerm 30 ref appTerm 52 ref 31 ref appTerm 53 ref appTerm 58 def appTerm appTerm 33 ref "Number.Natural.<=" const 34 remove constTerm 59 def 29 ref appTerm 60 def 27 ref appTerm 61 def appTerm 62 def 26 ref "Number.Natural.-" const 48 remove constTerm 63 def 27 ref appTerm 64 def 29 ref appTerm 65 def appTerm 29 ref appTerm "Number.GF(p).-" const 6 ref constTerm 66 def 30 ref appTerm 67 def 31 ref appTerm 68 def appTerm 31 ref appTerm appTerm 28 remove 63 ref 29 ref appTerm 69 def 27 ref appTerm 70 def appTerm 30 ref appTerm 66 ref 31 ref appTerm 30 ref appTerm 71 def appTerm appTerm appTerm appTerm appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 72 def refl 73 def 23 ref 0 ref 9 ref 0 ref 9 ref 13 ref cons opType 74 def nil cons cons opType constTerm 26 ref appTerm "select" const 75 def 0 ref 74 ref 9 ref nil cons 76 def cons opType constTerm 77 def 72 ref appTerm appTerm assume sym appThm 72 ref 26 remove appTerm betaConv trans "A" 76 remove cons nil cons 78 def nil nil cons 79 def cons nil 23 ref 0 ref 0 ref 0 ref "A" varType 80 def 13 ref cons opType 81 def 13 ref cons opType 82 def 0 ref 82 ref 13 ref cons opType 83 def nil cons cons opType constTerm 84 def "Data.Bool.?" const 85 def 82 ref constTerm 86 def appTerm 87 def "p" 81 ref var 88 def 88 ref varTerm 89 def 75 ref 0 ref 81 ref 80 ref nil cons 90 def cons opType constTerm 89 ref appTerm appTerm 91 def absTerm appTerm axiom subst 73 remove appThm "p" 74 ref var 92 def 92 remove varTerm 93 def 77 remove 93 remove appTerm appTerm absTerm 72 ref appTerm betaConv trans "h" 0 ref "Data.Pair.*" typeOp 94 def 1 ref 94 ref 1 ref 94 ref 4 remove opType 95 def nil cons 96 def cons opType 97 def nil cons 98 def cons opType 99 def 3 ref cons opType 100 def var 101 def 85 ref 0 ref 0 ref 100 ref 13 ref cons opType 102 def 13 ref cons opType 103 def constTerm 104 def "f" 100 ref var 105 def 11 ref 0 ref 0 ref 99 ref 13 ref cons opType 106 def 13 ref cons opType 107 def constTerm 108 def "x" 99 ref var 109 def 25 ref 105 ref varTerm 110 def 109 ref varTerm 111 def appTerm appTerm 112 def 33 ref 75 ref 0 ref 107 ref 106 ref nil cons 113 def cons opType constTerm 114 def "f" 106 ref var 115 def 15 ref 16 ref 15 ref 17 ref 20 ref 21 ref 20 ref 22 ref 23 ref 0 ref 12 ref 0 ref 12 ref 13 ref cons opType 116 def nil cons cons opType 117 def constTerm 118 def 115 remove varTerm "Data.Pair.," const 119 def 0 ref 1 ref 0 ref 97 ref 99 ref nil cons 120 def cons opType nil cons cons opType constTerm 121 def 27 ref appTerm 122 def 119 ref 0 ref 1 ref 0 ref 95 ref 98 ref cons opType nil cons cons opType constTerm 123 def 29 ref appTerm 124 def 119 ref 0 ref 2 ref 0 ref 2 ref 96 ref cons opType nil cons cons opType constTerm 125 def 30 ref appTerm 126 def 31 ref appTerm 127 def appTerm 128 def appTerm 129 def appTerm appTerm "Data.Bool./\\" const 117 ref constTerm 130 def "Data.Bool.~" const 116 ref constTerm 131 def 39 ref appTerm 132 def appTerm 133 def 131 ref 43 ref appTerm 134 def appTerm 135 def appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 136 def 111 ref appTerm appTerm 137 def 110 ref 75 ref 0 ref 0 ref 0 ref 99 ref 120 ref cons opType 138 def 13 ref cons opType 139 def 138 ref nil cons 140 def cons opType constTerm 141 def "f" 138 ref var 142 def 15 ref 16 ref 15 ref 17 ref 20 ref 21 ref 20 ref 22 ref 23 ref 0 ref 99 ref 113 ref cons opType constTerm 143 def 142 remove varTerm 129 ref appTerm appTerm 32 ref 0 ref 12 ref 0 ref 99 ref 140 ref cons opType nil cons cons opType constTerm 144 def 46 ref appTerm 145 def 121 ref 51 ref appTerm 146 def 124 ref 125 ref 54 ref appTerm 147 def 31 ref appTerm 148 def appTerm 149 def appTerm 150 def appTerm 144 ref 55 ref appTerm 151 def 122 ref 123 ref 57 ref appTerm 152 def 126 ref 58 ref appTerm 153 def appTerm 154 def appTerm 155 def appTerm 144 ref 61 ref appTerm 156 def 121 ref 65 ref appTerm 157 def 124 ref 125 ref 68 ref appTerm 158 def 31 ref appTerm 159 def appTerm 160 def appTerm 161 def appTerm 122 ref 123 ref 70 ref appTerm 162 def 126 ref 71 ref appTerm 163 def appTerm appTerm 164 def appTerm 165 def appTerm 166 def appTerm 167 def appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 168 def 111 ref appTerm appTerm appTerm 169 def 101 ref varTerm 111 ref appTerm 170 def appTerm appTerm absTerm appTerm absTerm appTerm absTerm 171 def 75 ref 0 ref 102 ref 100 ref nil cons 172 def cons opType constTerm 173 def 105 ref 15 ref 16 ref 15 ref 17 ref 20 ref 21 ref 20 ref 22 ref 25 ref 110 ref 129 ref appTerm appTerm 41 ref 31 ref appTerm 174 def appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 175 def appTerm 176 def betaConv "g" 138 ref var 177 def 11 ref 103 remove constTerm 178 def 101 ref 104 ref 105 ref 108 ref 109 ref 112 ref 137 remove 110 ref 177 ref varTerm 111 ref appTerm appTerm 179 def appTerm 170 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 180 def 168 ref appTerm 181 def betaConv "p" 106 ref var 182 def 11 ref 0 ref 139 ref 13 ref cons opType 183 def constTerm 184 def 177 remove 178 ref 101 remove 104 ref 105 ref 108 ref 109 ref 112 ref 33 ref 182 ref varTerm 111 ref appTerm appTerm 179 remove appTerm 170 remove appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 185 def 136 ref appTerm 186 def betaConv "A" 120 ref cons 187 def "B" 3 ref cons nil cons 188 def cons 79 ref cons nil 11 ref 83 remove constTerm 189 def 88 ref 11 ref 0 ref 0 ref 0 ref 80 ref 90 ref cons opType 190 def 13 ref cons opType 13 ref cons opType constTerm "g" 190 ref var 191 def 11 ref 0 ref 0 ref 0 ref 80 ref "B" varType 192 def nil cons 193 def cons 194 def opType 195 def 13 ref cons opType 196 def 13 ref cons opType 197 def constTerm 198 def "h" 195 ref var 199 def 85 ref 197 remove constTerm "f" 195 ref var 200 def 11 ref 82 ref constTerm 201 def "x" 80 ref var 202 def 23 ref 0 ref 192 ref 0 ref 192 ref 13 ref cons opType 203 def nil cons cons opType constTerm 204 def 200 remove varTerm 205 def 202 ref varTerm 206 def appTerm appTerm 32 ref 0 ref 12 ref 0 ref 192 ref 0 ref 192 ref 193 ref cons opType nil cons 207 def cons opType nil cons cons opType constTerm 89 ref 206 ref appTerm 208 def appTerm 205 remove 191 remove varTerm 206 ref appTerm appTerm appTerm 199 remove varTerm 206 ref appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm axiom subst nil "p" 12 ref var 209 def 11 ref 0 ref 107 ref 13 ref cons opType 210 def constTerm 185 ref appTerm nil cons cons "q" 12 ref var 211 def 186 remove nil cons cons nil cons cons nil cons cons 118 ref "Data.Bool.==>" const 117 ref constTerm 212 def 209 ref varTerm 213 def appTerm 214 def 211 ref varTerm 215 def appTerm 216 def appTerm 217 def refl 209 ref 211 ref 118 ref 130 ref 213 ref appTerm 218 def 215 ref appTerm 219 def appTerm 220 def 213 ref appTerm absTerm 221 def absTerm 222 def 213 ref appTerm betaConv 215 ref refl 223 def appThm 221 remove 215 ref appTerm betaConv trans appThm nil 23 ref 0 ref 117 ref 0 ref 117 ref 13 ref cons opType 224 def nil cons cons opType constTerm 225 def 212 ref appTerm 222 remove appTerm axiom 213 ref refl 226 def appThm 223 ref appThm eqMp 227 def sym 228 def 220 remove refl 211 ref 23 ref 0 ref 224 ref 0 ref 224 remove 13 ref cons opType nil cons cons opType constTerm 229 def "f" 117 ref var 230 def 230 ref varTerm 231 def 213 ref appTerm 215 ref appTerm absTerm 232 def appTerm 230 ref 231 ref "Data.Bool.T" const 12 ref constTerm 233 def appTerm 233 ref appTerm absTerm 234 def appTerm absTerm 235 def 215 ref appTerm betaConv appThm 23 ref 0 ref 116 ref 0 ref 116 ref 13 ref cons opType 236 def nil cons cons opType constTerm 237 def 218 remove appTerm refl 209 ref 235 remove absTerm 238 def 213 ref appTerm betaConv appThm nil 225 ref 130 ref appTerm 238 ref appTerm axiom 239 def 226 remove appThm eqMp 223 ref appThm eqMp 240 def sym 230 ref 231 ref refl nil "t" 12 ref var 241 def 213 ref nil cons 242 def cons nil cons nil cons cons 118 ref 241 ref varTerm 243 def appTerm 233 ref appTerm assume sym nil 233 ref axiom 244 def eqMp 243 ref assume 244 ref deductAntisym deductAntisym 245 def subst 213 ref assume 246 def eqMp appThm nil 241 ref 215 ref nil cons 247 def cons nil cons nil cons cons 245 ref subst 215 ref assume 248 def eqMp appThm absThm eqMp 249 def nil "P" 12 ref var 250 def 242 ref cons "Q" 12 ref var 251 def 247 ref cons nil cons 252 def cons nil cons cons 118 ref refl 253 def 230 ref 231 remove 250 ref varTerm 254 def appTerm 255 def 251 ref varTerm 256 def appTerm absTerm 257 def 209 ref 211 ref 213 ref absTerm absTerm 258 def appTerm betaConv 258 ref 254 ref appTerm betaConv 256 ref refl 259 def appThm 211 ref 254 ref absTerm 256 ref appTerm betaConv trans trans appThm 234 ref 258 ref appTerm betaConv 258 ref 233 ref appTerm betaConv 233 ref refl 260 def appThm 211 ref 233 ref absTerm 233 ref appTerm betaConv trans trans appThm 118 ref 130 ref 254 ref appTerm 261 def 256 ref appTerm 262 def appTerm refl 211 ref 229 remove 230 remove 255 remove 215 ref appTerm absTerm appTerm 234 ref appTerm absTerm 256 ref appTerm betaConv appThm 237 ref 261 remove appTerm refl 238 remove 254 ref appTerm betaConv appThm 239 remove 254 ref refl 263 def appThm eqMp 259 ref appThm eqMp 262 remove assume eqMp 264 def 258 remove refl appThm eqMp sym 244 ref eqMp 265 def subst 266 def deductAntisym eqMp 227 remove 216 ref assume eqMp sym 246 ref eqMp 253 ref 232 remove 209 ref 211 ref 215 ref absTerm 267 def absTerm 268 def appTerm betaConv 268 ref 213 ref appTerm betaConv 223 remove appThm 267 ref 215 ref appTerm betaConv trans trans appThm 234 remove 268 ref appTerm betaConv 268 ref 233 ref appTerm betaConv 260 remove appThm 267 ref 233 ref appTerm betaConv trans trans 269 def appThm 240 remove 219 remove assume eqMp 268 ref refl 270 def appThm eqMp sym 244 ref eqMp 271 def proveHyp 272 def deductAntisym 273 def subst proveHyp "A" 113 remove cons nil cons 274 def "P" 107 ref var 275 def 185 remove nil cons cons "x" 106 ref var 276 def 136 ref nil cons cons nil cons cons nil cons cons nil 209 ref 201 ref "P" 81 ref var 277 def varTerm 278 def appTerm 279 def nil cons 280 def cons 211 ref 278 ref 206 ref appTerm 281 def nil cons 282 def cons nil cons cons nil cons cons 283 def 228 ref subst 283 remove 271 remove 249 remove deductAntisym 284 def subst 118 ref 281 ref appTerm refl 202 ref 233 ref absTerm 285 def 206 ref appTerm betaConv appThm 88 ref 23 ref 0 ref 81 ref 82 ref nil cons cons opType constTerm 89 ref appTerm 285 remove appTerm absTerm 286 def 278 ref appTerm betaConv 287 def nil 84 remove 201 ref appTerm 286 remove appTerm axiom 278 ref refl 288 def appThm 289 def 279 ref assume eqMp eqMp 206 ref refl 290 def appThm eqMp sym 244 ref eqMp eqMp nil 250 ref 280 remove cons 251 ref 282 ref cons nil cons cons nil cons cons 265 ref subst deductAntisym eqMp 291 def subst eqMp eqMp nil 209 ref 184 remove 180 ref appTerm nil cons cons 211 ref 181 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp "A" 140 remove cons nil cons 292 def "P" 139 ref var 293 def 180 remove nil cons cons "x" 138 ref var 294 def 168 ref nil cons cons nil cons cons nil cons cons 291 ref subst eqMp eqMp nil 209 ref 178 ref 171 ref appTerm nil cons cons 211 ref 176 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp "A" 172 remove cons nil cons 295 def "P" 102 ref var 296 def 171 remove nil cons cons "x" 100 ref var 297 def 175 ref nil cons cons nil cons cons nil cons cons 291 ref subst eqMp eqMp nil 209 ref 104 ref 105 ref 108 ref 109 ref 112 remove 169 remove 175 ref 111 ref appTerm appTerm appTerm absTerm 298 def appTerm absTerm appTerm 299 def nil cons 300 def cons 211 ref 85 ref 0 ref 74 ref 13 ref cons opType constTerm 72 ref appTerm 301 def nil cons 302 def cons nil cons 303 def cons nil cons cons 304 def 273 ref subst proveHyp 304 ref 228 ref subst 304 remove 284 ref subst 104 ref refl 105 ref 253 ref 108 remove refl 109 remove 298 ref 111 remove appTerm betaConv absThm appThm appThm 15 ref refl 305 def "a" 1 ref var 306 def 11 ref 0 ref 0 ref 97 ref 13 ref cons opType 307 def 13 ref cons opType constTerm 308 def refl 309 def "b" 97 ref var 310 def 298 ref 121 ref 306 ref varTerm 311 def appTerm 312 def 310 ref varTerm 313 def appTerm 314 def appTerm betaConv absThm appThm absThm appThm appThm nil 182 remove 298 remove nil cons cons nil cons nil cons cons "A" 36 ref cons 315 def "B" 98 ref cons nil cons cons 79 ref cons 316 def "p" 0 ref 94 remove 194 remove opType 317 def 13 ref cons opType 318 def var 319 def 118 ref 11 ref 0 ref 318 ref 13 ref cons opType 320 def constTerm "x" 317 ref var 321 def 319 remove varTerm 322 def 321 remove varTerm appTerm absTerm appTerm appTerm 201 ref "a" 80 ref var 323 def 11 ref 0 ref 203 ref 13 ref cons opType constTerm 324 def "b" 192 ref var 325 def 322 ref 119 remove 0 ref 80 ref 0 ref 192 ref 317 ref nil cons cons opType nil cons cons opType constTerm 323 ref varTerm 326 def appTerm 325 ref varTerm 327 def appTerm 328 def appTerm absTerm appTerm absTerm appTerm appTerm absTerm 329 def 322 ref appTerm 330 def betaConv nil 11 ref 0 ref 320 ref 13 ref cons opType constTerm 329 ref appTerm 331 def axiom nil 209 ref 331 remove nil cons cons 211 ref 330 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp "A" 318 ref nil cons cons nil cons "P" 320 remove var 329 remove nil cons cons "x" 318 remove var 322 remove nil cons cons nil cons cons nil cons cons 291 ref subst eqMp eqMp 332 def subst subst eqMp 305 ref 306 ref 253 ref 309 remove 310 ref 310 ref 25 ref 110 ref 314 ref appTerm appTerm 33 ref 136 ref 314 ref appTerm appTerm 110 ref 168 ref 314 ref appTerm appTerm appTerm 175 ref 314 ref appTerm appTerm appTerm absTerm 333 def 313 ref appTerm betaConv absThm appThm appThm 305 ref "a'" 1 ref var 334 def 11 ref 0 ref 0 ref 95 ref 13 ref cons opType 335 def 13 ref cons opType constTerm 336 def refl 337 def "b" 95 ref var 338 def 333 ref 123 ref 334 ref varTerm 339 def appTerm 340 def 338 ref varTerm 341 def appTerm 342 def appTerm betaConv absThm appThm absThm appThm appThm nil "p" 307 ref var 333 remove nil cons cons nil cons nil cons cons 315 ref "B" 96 ref cons nil cons cons 79 ref cons 343 def 332 ref subst subst eqMp 305 remove 334 ref 253 ref 337 remove 338 ref 338 ref 25 ref 110 ref 312 ref 342 remove appTerm 344 def appTerm appTerm 33 ref 136 remove 344 ref appTerm appTerm 110 ref 168 remove 344 ref appTerm appTerm appTerm 175 remove 344 remove appTerm appTerm appTerm absTerm 345 def 341 ref appTerm betaConv absThm appThm appThm 20 ref refl 346 def "a" 2 ref var 347 def 346 ref "b" 2 ref var 348 def 345 ref 125 ref 347 ref varTerm 349 def appTerm 350 def 348 ref varTerm 351 def appTerm 352 def appTerm betaConv absThm appThm absThm appThm appThm nil "p" 335 ref var 345 remove nil cons cons nil cons nil cons cons "A" 3 ref cons 353 def 188 remove cons 79 ref cons 354 def 332 remove subst subst eqMp 346 ref 347 ref 346 remove 348 ref 25 ref 110 ref 312 ref 340 ref 352 ref appTerm appTerm 355 def appTerm appTerm 356 def refl 33 ref refl 357 def nil 22 ref 351 ref nil cons 358 def cons 21 ref 349 ref nil cons 359 def cons 17 ref 339 ref nil cons 360 def cons 16 ref 311 ref nil cons 361 def cons nil cons cons cons cons nil cons cons 362 def 22 ref 118 ref 114 remove "_30541" 106 remove var 363 def 15 ref 16 ref 15 ref 17 ref 20 ref 21 ref 20 ref 22 ref 118 ref 363 remove varTerm 129 ref appTerm appTerm 135 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 364 def appTerm 365 def 129 ref appTerm appTerm 135 ref appTerm absTerm 366 def 31 ref appTerm 367 def betaConv 21 ref 20 ref 366 ref appTerm 368 def absTerm 369 def 30 ref appTerm 370 def betaConv 17 ref 20 ref 369 ref appTerm 371 def absTerm 372 def 29 ref appTerm 373 def betaConv 16 ref 15 ref 372 ref appTerm 374 def absTerm 375 def 27 ref appTerm 376 def betaConv 364 ref 365 remove appTerm 377 def betaConv 364 ref "_30539" 99 ref var 378 def 130 ref 131 ref 35 ref 75 ref 0 ref 0 ref 0 ref 99 ref 36 ref cons opType 379 def 13 ref cons opType 379 ref nil cons cons opType constTerm "fn" 379 remove var 380 def 15 ref 306 ref 308 ref 310 ref 35 ref 380 remove varTerm 314 ref appTerm appTerm 311 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm 381 def 378 remove varTerm 382 def appTerm appTerm 38 ref appTerm appTerm appTerm 131 ref 35 ref 75 ref 0 ref 0 ref 0 ref 97 ref 36 remove cons opType 383 def 13 ref cons opType 383 ref nil cons cons opType constTerm "fn" 383 remove var 384 def 15 ref 306 ref 336 ref 338 ref 35 ref 384 remove varTerm 123 ref 311 ref appTerm 341 ref appTerm 385 def appTerm appTerm 311 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm 386 def 75 ref 0 ref 0 ref 0 ref 99 ref 98 remove cons opType 387 def 13 ref cons opType 387 ref nil cons cons opType constTerm "fn" 387 remove var 388 def 15 ref 306 ref 308 remove 310 ref 23 ref 0 ref 97 ref 307 remove nil cons cons opType constTerm 388 remove varTerm 314 remove appTerm appTerm 313 remove appTerm absTerm appTerm absTerm appTerm absTerm appTerm 389 def 382 remove appTerm appTerm appTerm 38 ref appTerm appTerm appTerm absTerm 390 def appTerm betaConv sym nil "P" 14 remove var 391 def 16 ref 15 ref 17 ref 20 ref 21 ref 20 ref 22 ref 118 ref 390 ref 129 ref appTerm 392 def appTerm 135 ref appTerm 393 def absTerm 394 def appTerm 395 def absTerm 396 def appTerm 397 def absTerm 398 def appTerm 399 def absTerm nil cons cons nil cons nil cons cons 315 remove nil cons 400 def 79 ref cons 401 def 118 ref 279 remove appTerm refl 287 remove appThm 289 remove eqMp sym 402 def subst 403 def subst 16 ref nil 241 ref 399 remove nil cons cons nil cons nil cons cons 245 ref subst nil 391 ref 398 remove nil cons cons nil cons nil cons cons 403 ref subst 17 ref nil 241 ref 397 remove nil cons cons nil cons nil cons cons 245 ref subst nil "P" 18 ref var 404 def 396 remove nil cons cons nil cons nil cons cons 353 remove nil cons 405 def 79 ref cons 406 def 402 ref subst 407 def subst 21 ref nil 241 ref 395 remove nil cons cons nil cons nil cons cons 245 ref subst nil 404 ref 394 remove nil cons cons nil cons nil cons cons 407 ref subst 22 ref nil 241 ref 393 remove nil cons cons nil cons nil cons cons 245 ref subst 392 remove betaConv 118 ref "_30534" 2 ref var 408 def 135 ref absTerm 409 def 31 ref appTerm 410 def appTerm refl 408 ref 130 ref 131 ref 35 ref 381 ref 129 ref appTerm 411 def appTerm 38 ref appTerm 412 def appTerm appTerm 413 def 131 ref 35 ref 386 ref 389 ref 129 ref appTerm 414 def appTerm 415 def appTerm 38 ref appTerm appTerm appTerm 416 def absTerm 417 def 75 ref 0 ref 0 ref 0 ref 95 ref 3 remove cons opType 418 def 13 ref cons opType 418 ref nil cons cons opType constTerm 419 def "fn" 418 remove var 420 def 20 ref 347 ref 20 ref 348 ref 25 ref 420 ref varTerm 352 remove appTerm appTerm 421 def 351 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm 422 def 75 ref 0 ref 0 ref 0 ref 97 ref 96 remove cons opType 423 def 13 ref cons opType 423 ref nil cons cons opType constTerm "fn" 423 remove var 424 def 15 ref 306 ref 336 remove 338 ref 23 ref 0 ref 95 ref 335 remove nil cons cons opType constTerm 424 remove varTerm 385 remove appTerm appTerm 341 remove appTerm absTerm appTerm absTerm appTerm absTerm appTerm 425 def 414 ref appTerm 426 def appTerm 427 def appTerm betaConv appThm 253 ref 410 remove betaConv appThm 416 remove refl appThm trans 23 ref 0 ref 18 remove 19 remove nil cons cons opType constTerm 428 def "_30533" 2 ref var 429 def 409 remove absTerm 30 ref appTerm 430 def appTerm refl 429 ref 417 ref absTerm 431 def 419 remove 420 remove 20 ref 347 ref 20 ref 348 ref 421 remove 349 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm 432 def 426 remove appTerm 433 def appTerm betaConv appThm 428 remove refl 430 remove betaConv appThm 417 remove refl appThm trans 23 ref 0 ref 24 ref 0 ref 24 ref 13 ref cons opType nil cons cons opType constTerm 434 def "_30532" 1 ref var 435 def 429 ref 408 ref 133 remove 131 ref 35 ref 435 ref varTerm appTerm 38 ref appTerm appTerm 436 def appTerm absTerm absTerm absTerm 29 ref appTerm 437 def appTerm refl 435 ref 429 ref 408 ref 413 remove 436 ref appTerm absTerm absTerm absTerm 438 def 415 ref appTerm betaConv appThm 434 remove refl 437 remove betaConv appThm 431 remove refl appThm trans 23 ref 0 ref 0 ref 1 ref 24 remove nil cons cons opType 439 def 0 ref 439 remove 13 ref cons opType nil cons cons opType constTerm 440 def "_30531" 1 ref var 441 def 435 remove 429 remove 408 remove 130 ref 131 ref 35 ref 441 remove varTerm appTerm 38 ref appTerm appTerm appTerm 436 remove appTerm absTerm absTerm absTerm absTerm 442 def 27 ref appTerm 443 def appTerm refl 442 ref 411 ref appTerm betaConv appThm 440 remove refl 443 remove betaConv appThm 438 remove refl appThm trans 442 remove refl nil 310 remove 128 ref nil cons cons 306 ref 27 ref nil cons 444 def cons nil cons 445 def cons nil cons cons 446 def 316 ref 325 ref 23 ref 0 ref 80 ref 81 ref nil cons 447 def cons opType constTerm 448 def 75 ref 0 ref 0 ref 0 ref 317 ref 90 ref cons opType 449 def 13 ref cons opType 450 def 449 ref nil cons 451 def cons opType constTerm "fn" 449 remove var 452 def 201 ref 323 ref 324 ref 325 ref 448 ref 452 ref varTerm 328 ref appTerm appTerm 453 def 326 ref appTerm absTerm appTerm absTerm appTerm absTerm 454 def appTerm 455 def 328 ref appTerm appTerm 326 ref appTerm absTerm 456 def 327 ref appTerm 457 def betaConv 323 ref 324 ref 456 ref appTerm 458 def absTerm 459 def 326 ref appTerm 460 def betaConv 454 ref 455 remove appTerm 461 def betaConv 85 ref 0 ref 450 ref 13 ref cons opType constTerm 462 def refl 452 remove 201 ref refl 463 def 323 ref 324 ref refl 464 def 325 ref 453 remove refl 323 ref 325 ref 326 ref absTerm 465 def absTerm 466 def 326 ref appTerm betaConv 327 ref refl 467 def appThm 465 remove 327 ref appTerm betaConv trans appThm absThm appThm absThm appThm absThm appThm "C" 90 ref cons nil cons "_1343" 0 ref 80 ref 0 ref 192 ref 90 ref cons opType nil cons cons opType var 466 remove nil cons cons nil cons nil cons cons nil "f" 0 ref 80 ref 0 ref 192 ref "C" varType 468 def nil cons 469 def cons opType nil cons cons opType 470 def var 471 def 323 ref 325 ref "_1343" 470 ref var varTerm 326 ref appTerm 327 ref appTerm 472 def absTerm 473 def absTerm 474 def nil cons cons nil cons nil cons cons 471 ref 85 ref 0 ref 0 ref 0 ref 317 ref 469 remove cons opType 475 def 13 ref cons opType 476 def 13 ref cons opType 477 def constTerm 478 def "fn" 475 ref var 479 def 201 ref 323 ref 324 ref 325 ref 23 ref 0 ref 468 ref 0 ref 468 remove 13 ref cons opType nil cons cons opType constTerm 479 ref varTerm 480 def 328 ref appTerm appTerm 481 def 471 remove varTerm 482 def 326 ref appTerm 327 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 483 def 482 ref appTerm 484 def betaConv nil 11 ref 0 ref 0 ref 470 ref 13 ref cons opType 485 def 13 ref cons opType constTerm 483 ref appTerm 486 def axiom nil 209 ref 486 remove nil cons cons 211 ref 484 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp "A" 470 ref nil cons cons nil cons "P" 485 remove var 483 remove nil cons cons "x" 470 remove var 482 remove nil cons cons nil cons cons nil cons cons 291 ref subst eqMp eqMp subst nil 209 ref 478 ref 479 ref 201 ref 323 ref 324 ref 325 ref 481 ref 474 remove 326 ref appTerm 487 def 327 ref appTerm appTerm absTerm appTerm absTerm appTerm 488 def absTerm 489 def appTerm 490 def nil cons cons 211 ref 478 remove 479 ref 201 ref 323 ref 324 ref 325 ref 481 ref 472 remove appTerm absTerm appTerm absTerm appTerm absTerm 491 def appTerm 492 def nil cons 493 def cons nil cons 494 def cons nil cons cons 273 ref subst nil "P" 476 remove var 495 def 479 ref 212 ref 489 ref 480 ref appTerm 496 def appTerm 492 ref appTerm 497 def absTerm nil cons cons nil cons nil cons cons "A" 475 ref nil cons cons nil cons 498 def 79 ref cons 402 ref subst subst 479 remove nil 241 ref 497 remove nil cons cons nil cons nil cons cons 245 ref subst nil 209 ref 496 ref nil cons 499 def cons 494 ref cons nil cons cons 500 def 228 ref subst 500 remove 284 ref subst 496 ref betaConv 496 remove assume eqMp nil 209 ref 488 ref nil cons 501 def cons 494 remove cons nil cons cons 502 def 273 ref subst proveHyp 502 ref 228 ref subst 502 remove 284 ref subst 491 ref 480 ref appTerm betaConv sym 463 ref 323 ref 464 ref 325 ref 481 remove refl 487 remove betaConv 467 ref appThm 473 remove 327 ref appTerm betaConv trans appThm absThm appThm absThm appThm 488 remove assume eqMp eqMp 498 ref 495 ref 491 remove nil cons cons "x" 475 remove var 503 def 480 remove nil cons cons nil cons cons nil cons cons 118 ref 86 ref 278 ref appTerm 504 def appTerm 505 def refl 88 ref 11 ref 236 remove constTerm 506 def 211 ref 212 ref 201 ref 202 ref 212 ref 208 ref appTerm 507 def 215 ref appTerm absTerm appTerm appTerm 215 ref appTerm absTerm appTerm absTerm 508 def 278 remove appTerm betaConv appThm nil 87 remove 508 remove appTerm axiom 288 remove appThm eqMp 509 def sym nil "P" 116 remove var 510 def 251 ref 212 ref 201 ref 202 ref 212 ref 281 ref appTerm 511 def 256 ref appTerm 512 def absTerm 513 def appTerm 514 def appTerm 515 def 256 ref appTerm 516 def absTerm nil cons cons nil cons nil cons cons "A" 13 ref cons nil cons 517 def 79 ref cons 402 ref subst 518 def subst 251 ref nil 241 ref 516 remove nil cons cons nil cons nil cons cons 245 ref subst nil 209 ref 514 ref nil cons 519 def cons 520 def 211 ref 256 ref nil cons 521 def cons nil cons 522 def cons nil cons cons 523 def 228 ref subst 523 ref 284 ref subst nil 209 ref 282 ref cons 522 ref cons nil cons cons 524 def 273 ref subst 525 def 513 ref 206 ref appTerm 526 def betaConv nil 520 ref 211 ref 526 remove nil cons cons nil cons cons nil cons cons 273 ref subst "A" 90 remove cons 527 def nil cons 528 def 277 ref 513 remove nil cons cons 529 def 202 ref 206 ref nil cons cons nil cons 530 def cons nil cons cons 291 ref subst eqMp eqMp 531 def eqMp eqMp nil 250 ref 519 ref cons 532 def 251 ref 521 ref cons nil cons 533 def cons nil cons cons 265 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp 534 def subst proveHyp eqMp nil 250 ref 501 remove cons 251 ref 493 remove cons nil cons 535 def cons nil cons cons 265 ref subst deductAntisym eqMp eqMp eqMp nil 250 ref 499 remove cons 535 ref cons nil cons cons 265 ref subst deductAntisym eqMp eqMp absThm eqMp nil 209 ref 11 remove 477 remove constTerm 503 ref 212 ref 489 ref 503 remove varTerm appTerm appTerm 492 ref appTerm absTerm appTerm nil cons cons 211 ref 212 ref 490 remove appTerm 492 remove appTerm nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp 498 remove 495 remove 489 remove nil cons cons 535 remove cons nil cons cons nil 520 ref 211 ref 212 ref 504 ref appTerm 536 def 256 ref appTerm nil cons 537 def cons nil cons cons nil cons cons 538 def 228 ref subst 538 remove 284 ref subst nil 209 ref 504 remove nil cons 539 def cons 540 def 522 ref cons nil cons cons 541 def 228 ref subst 541 remove 284 ref subst 523 remove 273 ref subst 211 ref 212 ref 201 ref 202 ref 511 remove 215 ref appTerm absTerm appTerm appTerm 215 ref appTerm absTerm 542 def 256 ref appTerm 543 def betaConv nil 540 remove 211 ref 506 ref 542 ref appTerm 544 def nil cons 545 def cons nil cons cons nil cons cons 546 def 273 ref subst 509 remove nil 209 ref 505 remove 544 ref appTerm nil cons cons 211 ref 536 remove 544 remove appTerm nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp 546 remove nil 209 ref 118 ref 213 ref appTerm 547 def 215 ref appTerm 548 def nil cons 549 def cons 550 def 211 ref 216 ref nil cons 551 def cons nil cons 552 def cons nil cons cons 553 def 228 ref subst 553 remove 284 ref subst 228 ref 284 ref 548 remove assume 554 def 246 remove eqMp eqMp 266 ref deductAntisym eqMp 555 def eqMp nil 250 ref 549 remove cons 556 def 251 ref 551 ref cons nil cons 557 def cons nil cons cons 265 ref subst deductAntisym eqMp 558 def subst eqMp eqMp nil 209 ref 545 remove cons 211 ref 543 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp 517 ref 510 ref 542 remove nil cons cons "x" 12 ref var 559 def 521 remove cons nil cons cons nil cons cons 291 ref subst eqMp eqMp eqMp eqMp nil 250 ref 539 remove cons 533 ref cons nil cons cons 265 ref subst deductAntisym eqMp eqMp nil 532 ref 251 ref 537 remove cons nil cons cons nil cons cons 265 ref subst deductAntisym eqMp 560 def subst eqMp eqMp proveHyp 561 def subst eqMp nil 209 ref 462 remove 454 ref appTerm nil cons cons 211 ref 461 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp "A" 451 remove cons nil cons "p" 450 remove var 454 remove nil cons cons nil cons nil cons cons nil 209 ref 86 ref 89 ref appTerm 562 def nil cons 563 def cons 564 def 211 ref 118 ref 91 ref appTerm 565 def 233 ref appTerm 566 def nil cons 567 def cons nil cons 568 def cons nil cons cons 569 def 228 ref subst 569 remove 284 ref subst 86 ref refl nil "t" 81 ref var 89 ref nil cons 570 def cons nil cons nil cons cons 527 remove "B" 13 ref cons nil cons cons 79 ref cons "t" 195 ref var 571 def 23 ref 0 ref 195 ref 196 ref nil cons cons opType constTerm 202 ref 571 remove varTerm 572 def 206 ref appTerm absTerm appTerm 572 ref appTerm absTerm 573 def 572 ref appTerm 574 def betaConv nil 198 remove 573 ref appTerm 575 def axiom nil 209 ref 575 remove nil cons cons 211 ref 574 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp "A" 195 ref nil cons cons nil cons "P" 196 remove var 573 remove nil cons cons "x" 195 remove var 572 remove nil cons cons nil cons cons nil cons cons 291 ref subst eqMp eqMp subst subst appThm nil 241 ref 563 ref cons nil cons nil cons cons 576 def 245 ref subst 562 ref assume eqMp trans sym 244 ref eqMp nil 209 ref 86 ref 202 ref 208 ref absTerm appTerm nil cons cons 568 ref cons nil cons cons 273 ref subst proveHyp nil 277 ref 570 ref cons 251 ref 567 remove cons nil cons 577 def cons nil cons cons nil 520 remove 211 ref 212 ref 86 remove 202 ref 281 ref absTerm 578 def appTerm 579 def appTerm 256 ref appTerm 580 def nil cons 581 def cons nil cons 582 def cons nil cons cons 583 def 555 remove nil 209 ref 551 ref cons 584 def 211 ref 212 ref 215 ref appTerm 585 def 213 ref appTerm nil cons 586 def cons nil cons 587 def cons nil cons cons 284 ref subst proveHyp 585 ref refl 554 remove appThm sym nil 209 ref 247 ref cons 588 def 211 ref 247 ref cons nil cons 589 def cons nil cons cons 590 def 228 ref subst 590 remove 284 ref subst 248 remove eqMp nil 250 ref 247 remove cons 252 ref cons nil cons cons 265 ref subst deductAntisym eqMp eqMp 591 def eqMp nil 588 ref 211 ref 242 ref cons nil cons 592 def cons nil cons cons 273 ref subst nil 250 ref 551 remove cons 593 def 251 ref 586 remove cons nil cons 594 def cons nil cons cons 595 def 253 remove 257 remove 268 ref appTerm betaConv 268 remove 254 ref appTerm betaConv 259 ref appThm 267 remove 256 ref appTerm betaConv trans trans appThm 269 remove appThm 264 remove 270 remove appThm eqMp sym 244 ref eqMp subst eqMp 273 ref 595 remove 265 ref subst eqMp deductAntisym deductAntisym 596 def subst 583 ref 228 ref subst 583 remove 284 ref subst nil 277 ref 202 ref 212 ref 578 ref 206 ref appTerm 597 def appTerm 256 ref appTerm 598 def absTerm 599 def nil cons cons nil cons nil cons cons 402 ref subst 202 ref nil 241 ref 598 remove nil cons cons nil cons nil cons cons 245 ref subst nil 209 ref 597 ref nil cons 600 def cons 522 ref cons nil cons cons 601 def 228 ref subst 601 remove 284 ref subst 597 ref betaConv 602 def 597 remove assume eqMp 525 remove proveHyp 531 remove eqMp eqMp nil 250 ref 600 remove cons 533 ref cons nil cons cons 265 ref subst deductAntisym eqMp eqMp absThm eqMp nil 209 ref 201 ref 599 remove appTerm nil cons cons 582 remove cons nil cons cons 273 ref subst proveHyp 528 ref 277 ref 578 remove nil cons cons 603 def 533 ref cons nil cons cons 560 ref subst eqMp eqMp nil 532 remove 251 ref 581 ref cons nil cons cons nil cons cons 265 ref subst deductAntisym eqMp nil 209 ref 515 remove 580 ref appTerm nil cons cons 211 ref 212 ref 580 ref appTerm 514 remove appTerm nil cons cons nil cons cons nil cons cons 284 ref subst proveHyp nil 209 ref 581 ref cons 211 ref 519 ref cons nil cons cons nil cons cons 604 def 228 ref subst 604 remove 284 ref subst nil 529 remove nil cons nil cons cons 402 ref subst 202 ref nil 241 ref 512 remove nil cons cons nil cons nil cons cons 245 ref subst 524 ref 228 ref subst 524 remove 284 ref subst 602 remove sym 281 remove assume eqMp 528 ref 603 remove 530 ref cons nil cons cons 534 ref subst proveHyp nil 209 ref 579 remove nil cons cons 522 remove cons nil cons cons 273 ref subst 580 remove assume eqMp proveHyp eqMp nil 250 ref 282 remove cons 533 remove cons nil cons cons 265 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp nil 250 ref 581 remove cons 251 ref 519 remove cons nil cons cons nil cons cons 265 ref subst deductAntisym eqMp eqMp eqMp subst nil 277 ref 202 ref 507 ref 566 ref appTerm 605 def absTerm nil cons cons nil cons nil cons cons 402 ref subst 202 ref nil 241 ref 605 remove nil cons cons nil cons nil cons cons 245 ref subst nil 209 ref 208 remove nil cons 606 def cons 607 def 568 remove cons nil cons cons 608 def 228 ref subst 608 remove 284 ref subst nil 241 ref 91 ref nil cons 609 def cons nil cons nil cons cons 245 ref subst nil 607 remove 211 ref 609 remove cons 610 def nil cons cons nil cons cons 273 ref subst 202 ref 507 remove 91 ref appTerm absTerm 611 def 206 ref appTerm 612 def betaConv 88 remove 201 ref 611 ref appTerm 613 def absTerm 614 def 89 remove appTerm 615 def betaConv nil 189 remove 614 ref appTerm 616 def axiom nil 209 ref 616 remove nil cons cons 211 ref 615 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp "A" 447 remove cons nil cons "P" 82 remove var 614 remove nil cons cons "x" 81 remove var 570 remove cons nil cons cons nil cons cons 291 ref subst eqMp eqMp nil 209 ref 613 remove nil cons cons 211 ref 612 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp 528 ref 277 ref 611 remove nil cons cons 530 remove cons nil cons cons 291 ref subst eqMp eqMp eqMp eqMp eqMp nil 250 ref 606 remove cons 577 ref cons nil cons cons 265 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp eqMp eqMp nil 250 ref 563 ref cons 577 remove cons nil cons cons 265 ref subst deductAntisym eqMp nil 209 ref 212 ref 562 ref appTerm 617 def 566 remove appTerm nil cons cons 211 ref 118 ref 617 ref 91 remove appTerm appTerm 618 def 617 ref 233 ref appTerm appTerm nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp nil "q'" 12 ref var 619 def 233 ref nil cons cons nil cons nil cons cons 562 ref refl nil 209 ref 118 ref 562 ref appTerm 620 def 562 remove appTerm nil cons cons 211 ref 212 ref 617 ref 565 remove 619 ref varTerm 621 def appTerm 622 def appTerm appTerm 618 ref 617 remove 621 ref appTerm appTerm appTerm nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp nil "p'" 12 ref var 623 def 563 remove cons nil cons nil cons cons 619 ref 212 ref 620 remove 623 ref varTerm 624 def appTerm appTerm 212 ref 212 ref 624 ref appTerm 625 def 622 remove appTerm appTerm 618 remove 625 ref 621 ref appTerm 626 def appTerm appTerm appTerm absTerm 627 def 621 ref appTerm 628 def betaConv 623 ref 506 ref 627 ref appTerm 629 def absTerm 630 def 624 ref appTerm 631 def betaConv nil 610 remove 564 remove nil cons cons nil cons cons nil 510 ref 623 ref 506 ref 619 ref 212 ref 547 remove 624 ref appTerm 632 def appTerm 212 ref 625 ref 118 ref 215 ref appTerm 621 ref appTerm 633 def appTerm 634 def appTerm 217 remove 626 ref appTerm 635 def appTerm 636 def appTerm 637 def absTerm 638 def appTerm 639 def absTerm nil cons cons nil cons nil cons cons 518 ref subst 623 remove nil 241 ref 639 remove nil cons cons nil cons nil cons cons 245 ref subst nil 510 ref 638 remove nil cons cons nil cons nil cons cons 518 remove subst 619 remove nil 241 ref 637 remove nil cons cons nil cons nil cons cons 245 ref subst nil 209 ref 632 remove nil cons 640 def cons 641 def 211 ref 636 remove nil cons 642 def cons nil cons cons nil cons cons 643 def 228 ref subst 643 remove 284 ref subst nil 209 ref 634 ref nil cons 644 def cons 211 ref 635 remove nil cons 645 def cons nil cons cons nil cons cons 646 def 228 ref subst 646 remove 284 ref subst nil 584 remove 211 ref 626 ref nil cons 647 def cons nil cons cons nil cons cons 648 def 596 ref subst 648 ref 228 ref subst 648 remove 284 ref subst nil 209 ref 624 ref nil cons 649 def cons 650 def 211 ref 621 ref nil cons 651 def cons nil cons 652 def cons nil cons cons 653 def 228 ref subst 653 ref 284 ref subst nil 641 ref 211 ref 214 ref 624 remove appTerm 654 def nil cons 655 def cons nil cons cons nil cons cons 273 ref subst nil 209 ref 242 remove cons 211 ref 649 ref cons nil cons cons nil cons cons 656 def 558 ref subst eqMp 657 def nil 209 ref 655 ref cons 658 def 652 ref cons nil cons cons 659 def 273 ref subst proveHyp nil 641 remove 211 ref 625 remove 213 ref appTerm 660 def nil cons 661 def cons nil cons cons nil cons cons 273 ref subst 656 ref nil 550 remove 587 remove cons nil cons cons 662 def 228 ref subst 662 remove 284 ref subst 591 remove eqMp nil 556 remove 594 remove cons nil cons cons 265 ref subst deductAntisym eqMp 663 def subst eqMp 664 def nil 209 ref 661 ref cons 665 def 211 ref 212 ref 654 ref appTerm 666 def 621 ref appTerm nil cons 667 def cons nil cons cons nil cons cons 668 def 273 ref subst proveHyp 668 ref 228 ref subst 668 remove 284 ref subst 659 ref 228 ref subst 659 remove 284 ref subst nil 650 ref 592 remove cons nil cons cons 273 ref subst 660 remove assume eqMp 669 def 656 remove 273 ref subst 654 remove assume eqMp 670 def 669 remove proveHyp proveHyp nil 650 remove 211 ref 633 remove nil cons 671 def cons nil cons cons nil cons cons 273 ref subst 634 remove assume eqMp 672 def nil 209 ref 671 remove cons 673 def 211 ref 585 ref 621 ref appTerm 674 def nil cons 675 def cons nil cons cons nil cons cons 273 ref subst proveHyp nil 588 remove 652 ref cons nil cons cons 676 def 558 remove subst eqMp 677 def nil 209 ref 675 ref cons 678 def 652 remove cons nil cons cons 679 def 273 ref subst proveHyp 672 remove nil 673 remove 211 ref 212 ref 621 ref appTerm 215 ref appTerm 680 def nil cons 681 def cons nil cons cons nil cons cons 273 ref subst proveHyp 676 ref 663 remove subst eqMp 682 def nil 209 ref 681 ref cons 683 def 211 ref 212 ref 674 ref appTerm 684 def 621 remove appTerm nil cons 685 def cons nil cons cons nil cons cons 686 def 273 ref subst proveHyp 686 ref 228 ref subst 686 remove 284 ref subst 679 ref 228 ref subst 679 remove 284 ref subst 272 remove 676 remove 273 ref subst 674 remove assume eqMp proveHyp eqMp nil 250 ref 675 remove cons 687 def 251 ref 651 ref cons nil cons 688 def cons nil cons cons 265 ref subst deductAntisym eqMp eqMp nil 250 ref 681 remove cons 689 def 251 ref 685 remove cons nil cons cons nil cons cons 265 ref subst deductAntisym eqMp eqMp eqMp proveHyp eqMp nil 250 ref 655 remove cons 690 def 688 ref cons nil cons cons 265 ref subst deductAntisym eqMp eqMp nil 250 ref 661 remove cons 691 def 251 ref 667 remove cons nil cons cons nil cons cons 265 ref subst deductAntisym eqMp eqMp eqMp eqMp nil 250 ref 649 ref cons 688 remove cons nil cons cons 265 ref subst deductAntisym eqMp eqMp nil 593 remove 251 ref 647 ref cons nil cons cons nil cons cons 265 ref subst deductAntisym eqMp nil 209 ref 212 ref 216 ref appTerm 626 ref appTerm nil cons cons 211 ref 212 ref 626 ref appTerm 216 remove appTerm nil cons cons nil cons cons nil cons cons 284 ref subst proveHyp nil 209 ref 647 ref cons 552 remove cons nil cons cons 692 def 228 ref subst 692 remove 284 ref subst 228 ref 284 ref 657 remove nil 658 remove 589 ref cons nil cons cons 693 def 273 ref subst proveHyp 664 remove nil 665 remove 211 ref 666 remove 215 ref appTerm nil cons 694 def cons nil cons cons nil cons cons 695 def 273 ref subst proveHyp 695 ref 228 ref subst 695 remove 284 ref subst 693 ref 228 ref subst 693 remove 284 ref subst 670 remove 677 remove nil 678 remove 589 ref cons nil cons cons 696 def 273 ref subst proveHyp 682 remove nil 683 remove 211 ref 684 remove 215 remove appTerm nil cons 697 def cons nil cons cons nil cons cons 698 def 273 ref subst proveHyp 698 ref 228 ref subst 698 remove 284 ref subst 696 ref 228 ref subst 696 remove 284 ref subst 653 remove 273 ref subst 626 remove assume eqMp nil 209 ref 651 ref cons 589 remove cons nil cons cons 273 ref subst 680 remove assume eqMp proveHyp eqMp nil 687 remove 252 ref cons nil cons cons 265 ref subst deductAntisym eqMp eqMp nil 689 remove 251 ref 697 remove cons nil cons cons nil cons cons 265 ref subst deductAntisym eqMp eqMp eqMp proveHyp eqMp nil 690 remove 252 remove cons nil cons cons 265 ref subst deductAntisym eqMp eqMp nil 691 remove 251 ref 694 remove cons nil cons cons nil cons cons 265 ref subst deductAntisym eqMp eqMp eqMp eqMp 266 remove deductAntisym eqMp eqMp nil 250 ref 647 remove cons 557 remove cons nil cons cons 265 ref subst deductAntisym eqMp eqMp eqMp eqMp nil 250 ref 644 remove cons 251 ref 645 remove cons nil cons cons nil cons cons 265 ref subst deductAntisym eqMp eqMp nil 250 ref 640 remove cons 251 ref 642 remove cons nil cons cons nil cons cons 265 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp absThm eqMp subst nil 209 ref 506 ref 630 ref appTerm nil cons cons 211 ref 631 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp 517 ref 510 ref 630 remove nil cons cons 559 ref 649 remove cons nil cons cons nil cons cons 291 ref subst eqMp eqMp nil 209 ref 629 remove nil cons cons 211 ref 628 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp 517 ref 510 ref 627 remove nil cons cons 559 ref 651 remove cons nil cons cons nil cons cons 291 ref subst eqMp eqMp subst eqMp subst eqMp 576 remove 241 ref 118 ref 212 ref 243 ref appTerm 233 ref appTerm appTerm 233 ref appTerm absTerm 699 def 243 ref appTerm 700 def betaConv nil 506 ref 699 ref appTerm 701 def axiom nil 209 ref 701 remove nil cons cons 211 ref 700 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp 517 ref 510 ref 699 remove nil cons cons 559 ref 243 ref nil cons cons nil cons 702 def cons nil cons cons 291 ref subst eqMp eqMp subst trans sym 244 ref eqMp 703 def subst eqMp eqMp nil 209 ref 201 ref 459 ref appTerm nil cons cons 211 ref 460 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp 528 ref 277 ref 459 remove nil cons cons 202 ref 326 ref nil cons cons nil cons 704 def cons nil cons cons 291 ref subst eqMp eqMp nil 209 ref 458 remove nil cons cons 211 ref 457 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp "A" 193 ref cons nil cons 705 def "P" 203 remove var 706 def 456 remove nil cons cons "x" 192 remove var 327 ref nil cons cons nil cons 707 def cons nil cons cons 291 ref subst eqMp eqMp sym 708 def subst subst 709 def appThm eqMp 42 remove refl 35 ref "_30525" 97 ref var 710 def 386 ref 710 remove varTerm appTerm absTerm 711 def 128 ref appTerm 712 def appTerm refl 711 ref 414 ref appTerm betaConv appThm 35 ref refl 713 def 712 remove betaConv appThm 415 ref refl appThm trans 711 remove refl 446 remove 316 remove 325 ref 204 ref 75 remove 0 ref 0 ref 0 ref 317 remove 193 ref cons opType 714 def 13 ref cons opType 715 def 714 ref nil cons 716 def cons opType constTerm "fn" 714 remove var 717 def 201 ref 323 ref 324 ref 325 ref 204 remove 717 ref varTerm 328 ref appTerm appTerm 718 def 327 ref appTerm absTerm appTerm absTerm appTerm absTerm 719 def appTerm 720 def 328 remove appTerm appTerm 327 ref appTerm absTerm 721 def 327 ref appTerm 722 def betaConv 323 ref 324 remove 721 ref appTerm 723 def absTerm 724 def 326 ref appTerm 725 def betaConv 719 ref 720 remove appTerm 726 def betaConv 85 ref 0 ref 715 ref 13 ref cons opType constTerm 727 def refl 717 remove 463 remove 323 ref 464 remove 325 ref 718 remove refl 323 remove 325 remove 327 ref absTerm 728 def absTerm 729 def 326 remove appTerm betaConv 467 remove appThm 728 remove 327 remove appTerm betaConv trans appThm absThm appThm absThm appThm absThm appThm "C" 193 remove cons nil cons "_1343" 0 ref 80 ref 207 remove cons opType var 729 remove nil cons cons nil cons nil cons cons 561 remove subst eqMp nil 209 ref 727 remove 719 ref appTerm nil cons cons 211 ref 726 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp "A" 716 remove cons nil cons "p" 715 remove var 719 remove nil cons cons nil cons nil cons cons 703 ref subst eqMp eqMp nil 209 ref 201 ref 724 ref appTerm nil cons cons 211 ref 725 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp 528 ref 277 ref 724 remove nil cons cons 704 remove cons nil cons cons 291 ref subst eqMp eqMp nil 209 ref 723 remove nil cons cons 211 ref 722 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp 705 remove 706 remove 721 remove nil cons cons 707 remove cons nil cons cons 291 ref subst eqMp eqMp sym 730 def subst subst 731 def appThm eqMp appThm nil 338 remove 127 ref nil cons cons 306 ref 29 ref nil cons 732 def cons nil cons cons nil cons cons 733 def 343 ref 708 ref subst subst eqMp 734 def appThm eqMp 25 ref 30 ref appTerm refl 735 def 25 ref "_30527" 97 ref var 736 def 432 ref 425 ref 736 remove varTerm appTerm appTerm absTerm 737 def 128 ref appTerm 738 def appTerm refl 737 ref 414 ref appTerm betaConv appThm 25 ref refl 739 def 738 remove betaConv appThm 433 ref refl appThm trans 737 remove refl 731 ref appThm eqMp appThm 735 remove 25 ref "_30521" 95 ref var 740 def 432 ref 740 remove varTerm appTerm absTerm 741 def 127 ref appTerm 742 def appTerm refl 741 ref 425 ref 128 ref appTerm 743 def appTerm betaConv appThm 739 ref 742 remove betaConv appThm 432 ref 743 ref appTerm refl appThm trans 741 remove refl 733 remove 343 remove 730 ref subst subst 744 def appThm eqMp appThm nil 348 ref 31 ref nil cons 745 def cons 746 def 347 ref 30 ref nil cons 747 def cons 748 def nil cons cons nil cons cons 749 def 354 ref 708 remove subst subst eqMp eqMp 750 def appThm eqMp 25 ref 31 ref appTerm refl 751 def 25 ref "_30529" 97 remove var 752 def 422 ref 425 ref 752 remove varTerm appTerm appTerm absTerm 753 def 128 ref appTerm 754 def appTerm refl 753 ref 414 remove appTerm betaConv appThm 739 ref 754 remove betaConv appThm 427 ref refl appThm trans 753 remove refl 731 remove appThm eqMp appThm 751 remove 25 ref "_30523" 95 remove var 755 def 422 ref 755 remove varTerm appTerm absTerm 756 def 127 ref appTerm 757 def appTerm refl 756 ref 743 ref appTerm betaConv appThm 739 ref 757 remove betaConv appThm 422 ref 743 remove appTerm refl appThm trans 756 remove refl 744 remove appThm eqMp appThm 749 remove 354 remove 730 remove subst subst eqMp eqMp 758 def appThm eqMp sym trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp 274 ref 275 remove 364 ref nil cons 759 def cons 276 remove 390 remove nil cons cons nil cons cons nil cons cons 534 ref subst proveHyp nil 209 ref 85 ref 210 remove constTerm 364 remove appTerm nil cons cons 211 ref 377 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp nil "p" 107 remove var 759 remove cons nil cons nil cons cons 274 remove 79 ref cons 703 ref subst subst eqMp eqMp nil 209 ref 15 ref 375 ref appTerm nil cons cons 211 ref 376 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp 400 ref 391 ref 375 remove nil cons cons "x" 1 ref var 760 def 444 remove cons nil cons 761 def cons nil cons cons 291 ref subst eqMp eqMp nil 209 ref 374 remove nil cons cons 211 ref 373 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp 400 ref 391 ref 372 remove nil cons cons 760 ref 732 ref cons nil cons 762 def cons nil cons cons 291 ref subst eqMp eqMp nil 209 ref 371 remove nil cons cons 211 ref 370 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp 405 ref 404 ref 369 remove nil cons cons "x" 2 ref var 763 def 747 ref cons nil cons 764 def cons nil cons cons 291 ref subst eqMp eqMp nil 209 ref 368 remove nil cons cons 211 ref 367 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp 405 ref 404 ref 366 remove nil cons cons 763 ref 745 ref cons nil cons 765 def cons nil cons cons 291 ref subst eqMp eqMp subst appThm 110 ref refl 362 ref 22 ref 143 ref 141 remove "_30571" 138 remove var 766 def 15 ref 16 ref 15 ref 17 ref 20 ref 21 ref 20 ref 22 ref 143 ref 766 remove varTerm 129 ref appTerm appTerm 167 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 767 def appTerm 768 def 129 ref appTerm appTerm 167 ref appTerm absTerm 769 def 31 ref appTerm 770 def betaConv 21 ref 20 ref 769 ref appTerm 771 def absTerm 772 def 30 ref appTerm 773 def betaConv 17 ref 20 ref 772 ref appTerm 774 def absTerm 775 def 29 ref appTerm 776 def betaConv 16 ref 15 ref 775 ref appTerm 777 def absTerm 778 def 27 ref appTerm 779 def betaConv 767 ref 768 remove appTerm 780 def betaConv 767 ref "_30569" 99 ref var 781 def 144 ref 45 ref 381 ref 781 remove varTerm 782 def appTerm 783 def appTerm appTerm 121 ref 49 ref 783 ref appTerm 50 ref appTerm appTerm 123 ref 386 remove 389 ref 782 remove appTerm 784 def appTerm 785 def appTerm 786 def 125 ref 52 ref 432 ref 425 ref 784 remove appTerm 787 def appTerm 788 def appTerm 53 ref appTerm appTerm 422 ref 787 remove appTerm 789 def appTerm appTerm appTerm appTerm 144 ref 45 ref 785 ref appTerm appTerm 121 ref 783 ref appTerm 790 def 123 ref 49 ref 785 ref appTerm 50 ref appTerm appTerm 125 ref 788 ref appTerm 791 def 52 ref 789 ref appTerm 53 ref appTerm appTerm appTerm appTerm appTerm 144 ref 59 ref 785 ref appTerm 783 ref appTerm appTerm 121 ref 63 ref 783 ref appTerm 785 ref appTerm appTerm 786 remove 125 ref 66 ref 788 ref appTerm 789 ref appTerm appTerm 789 ref appTerm appTerm appTerm appTerm 790 remove 123 ref 63 ref 785 remove appTerm 783 remove appTerm appTerm 791 remove 66 ref 789 remove appTerm 788 remove appTerm appTerm appTerm appTerm appTerm appTerm appTerm absTerm 792 def appTerm betaConv sym nil 391 ref 16 ref 15 ref 17 ref 20 ref 21 ref 20 ref 22 ref 143 ref 792 ref 129 ref appTerm 793 def appTerm 167 ref appTerm 794 def absTerm 795 def appTerm 796 def absTerm 797 def appTerm 798 def absTerm 799 def appTerm 800 def absTerm nil cons cons nil cons nil cons cons 403 ref subst 16 ref nil 241 ref 800 remove nil cons cons nil cons nil cons cons 245 ref subst nil 391 ref 799 remove nil cons cons nil cons nil cons cons 403 ref subst 17 ref nil 241 ref 798 remove nil cons cons nil cons nil cons cons 245 ref subst nil 404 ref 797 remove nil cons cons nil cons nil cons cons 407 ref subst 21 ref nil 241 ref 796 remove nil cons cons nil cons nil cons cons 245 ref subst nil 404 ref 795 remove nil cons cons nil cons nil cons cons 407 ref subst 22 ref nil 241 ref 794 remove nil cons cons nil cons nil cons cons 245 ref subst 793 remove betaConv 143 ref "_30564" 2 ref var 801 def 145 ref 146 ref 124 ref 147 remove 801 ref varTerm 802 def appTerm appTerm appTerm appTerm 151 ref 122 ref 152 ref 126 ref 52 ref 802 ref appTerm 53 ref appTerm 803 def appTerm appTerm appTerm appTerm 156 ref 157 ref 124 ref 125 ref 67 remove 802 ref appTerm appTerm 802 ref appTerm appTerm appTerm appTerm 122 ref 162 ref 126 remove 66 ref 802 ref appTerm 804 def 30 ref appTerm appTerm appTerm appTerm appTerm appTerm appTerm absTerm 31 ref appTerm 805 def appTerm refl 801 ref 144 ref 45 ref 411 ref appTerm appTerm 806 def 121 ref 49 ref 411 ref appTerm 50 ref appTerm appTerm 807 def 123 ref 415 ref appTerm 808 def 125 ref 52 ref 433 ref appTerm 53 ref appTerm appTerm 809 def 802 ref appTerm appTerm appTerm appTerm 144 ref 45 ref 415 ref appTerm appTerm 810 def 121 ref 411 ref appTerm 811 def 123 ref 49 ref 415 ref appTerm 50 ref appTerm appTerm 812 def 125 ref 433 ref appTerm 813 def 803 ref appTerm appTerm appTerm appTerm 144 ref 59 ref 415 ref appTerm 411 ref appTerm appTerm 814 def 121 ref 63 ref 411 ref appTerm 815 def 415 ref appTerm appTerm 816 def 808 ref 125 ref 66 ref 433 ref appTerm 817 def 802 ref appTerm appTerm 802 ref appTerm appTerm appTerm appTerm 811 ref 123 ref 63 ref 415 ref appTerm 411 ref appTerm appTerm 818 def 813 ref 804 ref 433 ref appTerm appTerm appTerm appTerm appTerm appTerm appTerm absTerm 819 def 427 ref appTerm betaConv appThm 143 remove refl 805 remove betaConv appThm 806 ref 807 ref 808 ref 809 remove 427 ref appTerm appTerm appTerm appTerm 810 ref 811 ref 812 ref 813 ref 52 ref 427 ref appTerm 53 ref appTerm appTerm appTerm appTerm appTerm 814 ref 816 ref 808 ref 125 ref 817 remove 427 ref appTerm appTerm 427 ref appTerm appTerm appTerm appTerm 811 ref 818 ref 813 remove 66 ref 427 ref appTerm 433 ref appTerm appTerm appTerm appTerm appTerm appTerm appTerm refl appThm trans 23 ref 0 ref 0 ref 2 ref 120 remove cons opType 820 def 0 ref 820 ref 13 ref cons opType nil cons cons opType constTerm 821 def "_30563" 2 ref var 822 def 801 ref 145 ref 146 ref 124 ref 125 ref 52 ref 822 ref varTerm 823 def appTerm 53 ref appTerm appTerm 802 ref appTerm 824 def appTerm appTerm appTerm 151 ref 122 ref 152 ref 125 ref 823 ref appTerm 825 def 803 remove appTerm 826 def appTerm appTerm appTerm 156 remove 157 ref 124 ref 125 ref 66 ref 823 ref appTerm 802 ref appTerm appTerm 802 remove appTerm 827 def appTerm appTerm appTerm 122 ref 162 ref 825 remove 804 remove 823 remove appTerm appTerm 828 def appTerm appTerm appTerm appTerm appTerm absTerm absTerm 30 ref appTerm 829 def appTerm refl 822 ref 801 ref 806 ref 807 ref 808 ref 824 ref appTerm appTerm appTerm 810 remove 811 ref 812 remove 826 ref appTerm appTerm appTerm 814 remove 816 remove 808 remove 827 ref appTerm appTerm appTerm 811 ref 818 remove 828 ref appTerm appTerm appTerm appTerm appTerm absTerm absTerm 830 def 433 ref appTerm betaConv appThm 821 remove refl 829 remove betaConv appThm 819 remove refl appThm trans 23 ref 0 ref 0 ref 2 ref 820 remove nil cons cons opType 831 def 0 ref 831 ref 13 ref cons opType nil cons cons opType constTerm 832 def "_30562" 1 ref var 833 def 822 ref 801 ref 145 ref 146 ref 123 ref 833 ref varTerm 834 def appTerm 835 def 824 remove appTerm 836 def appTerm appTerm 144 ref 45 ref 834 ref appTerm appTerm 837 def 122 ref 123 ref 49 ref 834 ref appTerm 50 ref appTerm appTerm 826 remove appTerm 838 def appTerm appTerm 144 ref 59 ref 834 ref appTerm 839 def 27 ref appTerm appTerm 121 ref 64 ref 834 ref appTerm appTerm 835 remove 827 remove appTerm 840 def appTerm appTerm 122 ref 123 ref 63 ref 834 ref appTerm 841 def 27 ref appTerm appTerm 828 ref appTerm appTerm appTerm appTerm appTerm absTerm absTerm absTerm 29 ref appTerm 842 def appTerm refl 833 ref 822 ref 801 ref 806 remove 807 remove 836 ref appTerm appTerm 837 ref 811 ref 838 ref appTerm appTerm 144 ref 839 ref 411 ref appTerm appTerm 121 ref 815 remove 834 ref appTerm appTerm 840 ref appTerm appTerm 811 remove 123 ref 841 ref 411 ref appTerm appTerm 828 ref appTerm appTerm appTerm appTerm appTerm absTerm absTerm absTerm 843 def 415 ref appTerm betaConv appThm 832 remove refl 842 remove betaConv appThm 830 remove refl appThm trans 23 ref 0 ref 0 ref 1 ref 831 remove nil cons cons opType 844 def 0 ref 844 remove 13 ref cons opType nil cons cons opType constTerm 845 def "_30561" 1 ref var 846 def 833 remove 822 remove 801 remove 144 ref 45 ref 846 remove varTerm 847 def appTerm appTerm 121 ref 49 ref 847 ref appTerm 50 ref appTerm appTerm 836 remove appTerm appTerm 837 remove 121 ref 847 ref appTerm 848 def 838 remove appTerm appTerm 144 ref 839 remove 847 ref appTerm appTerm 121 ref 63 ref 847 ref appTerm 834 remove appTerm appTerm 840 remove appTerm appTerm 848 remove 123 ref 841 remove 847 remove appTerm appTerm 828 remove appTerm appTerm appTerm appTerm appTerm absTerm absTerm absTerm absTerm 849 def 27 ref appTerm 850 def appTerm refl 849 ref 411 ref appTerm betaConv appThm 845 remove refl 850 remove betaConv appThm 843 remove refl appThm trans 849 remove refl 709 ref appThm eqMp 734 ref appThm eqMp 750 ref appThm eqMp 758 ref appThm eqMp sym trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp 292 ref 293 remove 767 ref nil cons 851 def cons 294 remove 792 remove nil cons cons nil cons cons nil cons cons 534 ref subst proveHyp nil 209 ref 85 remove 183 remove constTerm 767 remove appTerm nil cons cons 211 ref 780 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp nil "p" 139 remove var 851 remove cons nil cons nil cons cons 292 remove 79 ref cons 703 ref subst subst eqMp eqMp nil 209 ref 15 ref 778 ref appTerm nil cons cons 211 ref 779 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp 400 ref 391 ref 778 remove nil cons cons 761 ref cons nil cons cons 291 ref subst eqMp eqMp nil 209 ref 777 remove nil cons cons 211 ref 776 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp 400 ref 391 ref 775 remove nil cons cons 762 ref cons nil cons cons 291 ref subst eqMp eqMp nil 209 ref 774 remove nil cons cons 211 ref 773 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp 405 ref 404 ref 772 remove nil cons cons 764 ref cons nil cons cons 291 ref subst eqMp eqMp nil 209 ref 771 remove nil cons cons 211 ref 770 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp 405 ref 404 ref 769 remove nil cons cons 765 ref cons nil cons cons 291 ref subst eqMp eqMp subst appThm appThm 362 remove 22 ref 25 ref 173 remove "_30601" 100 ref var 852 def 15 ref 16 ref 15 ref 17 ref 20 ref 21 ref 20 ref 22 ref 25 ref 852 remove varTerm 129 ref appTerm appTerm 174 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 853 def appTerm 854 def 129 ref appTerm appTerm 174 ref appTerm absTerm 855 def 31 ref appTerm 856 def betaConv 21 ref 20 ref 855 ref appTerm 857 def absTerm 858 def 30 ref appTerm 859 def betaConv 17 ref 20 ref 858 ref appTerm 860 def absTerm 861 def 29 ref appTerm 862 def betaConv 16 ref 15 ref 861 ref appTerm 863 def absTerm 864 def 27 ref appTerm 865 def betaConv 853 ref 854 remove appTerm 866 def betaConv 853 ref "_30599" 99 ref var 867 def 33 ref 35 ref 381 remove 867 remove varTerm 868 def appTerm appTerm 38 ref appTerm appTerm 432 remove 425 remove 389 remove 868 remove appTerm appTerm 869 def appTerm appTerm 422 remove 869 remove appTerm appTerm absTerm 870 def appTerm betaConv sym nil 391 ref 16 ref 15 ref 17 ref 20 ref 21 ref 20 ref 22 ref 25 ref 870 ref 129 ref appTerm 871 def appTerm 174 ref appTerm 872 def absTerm 873 def appTerm 874 def absTerm 875 def appTerm 876 def absTerm 877 def appTerm 878 def absTerm nil cons cons nil cons nil cons cons 403 ref subst 16 ref nil 241 ref 878 remove nil cons cons nil cons nil cons cons 245 ref subst nil 391 ref 877 remove nil cons cons nil cons nil cons cons 403 ref subst 17 ref nil 241 ref 876 remove nil cons cons nil cons nil cons cons 245 ref subst nil 404 ref 875 remove nil cons cons nil cons nil cons cons 407 ref subst 21 ref nil 241 ref 874 remove nil cons cons nil cons nil cons cons 245 ref subst nil 404 ref 873 remove nil cons cons nil cons nil cons cons 407 ref subst 22 ref nil 241 ref 872 remove nil cons cons nil cons nil cons cons 245 ref subst 871 remove betaConv 25 ref "_30594" 2 ref var 879 def 41 ref 879 ref varTerm 880 def appTerm absTerm 31 ref appTerm 881 def appTerm refl 879 ref 33 ref 412 remove appTerm 882 def 433 ref appTerm 883 def 880 ref appTerm absTerm 884 def 427 ref appTerm betaConv appThm 739 ref 881 remove betaConv appThm 883 remove 427 remove appTerm refl appThm trans 23 ref 0 ref 5 ref 0 ref 5 remove 13 ref cons opType nil cons cons opType constTerm 885 def "_30593" 2 ref var 886 def 879 ref 40 remove 886 ref varTerm 887 def appTerm 880 ref appTerm absTerm absTerm 888 def 30 ref appTerm 889 def appTerm refl 886 ref 879 ref 882 remove 887 ref appTerm 880 ref appTerm absTerm absTerm 890 def 433 remove appTerm betaConv appThm 885 remove refl 889 remove betaConv appThm 884 remove refl appThm trans 23 ref 0 ref 6 ref 0 ref 6 remove 13 ref cons opType nil cons cons opType constTerm 891 def "_30592" 1 ref var 892 def 888 remove absTerm 29 ref appTerm 893 def appTerm refl 892 ref 890 ref absTerm 894 def 415 remove appTerm betaConv appThm 891 remove refl 893 remove betaConv appThm 890 remove refl appThm trans 23 remove 0 ref 8 ref 0 ref 8 remove 13 remove cons opType nil cons cons opType constTerm 895 def "_30591" 1 ref var 896 def 892 remove 886 remove 879 remove 33 ref 35 ref 896 remove varTerm appTerm 38 ref appTerm appTerm 887 remove appTerm 880 remove appTerm absTerm absTerm absTerm absTerm 897 def 27 ref appTerm 898 def appTerm refl 897 ref 411 remove appTerm betaConv appThm 895 remove refl 898 remove betaConv appThm 894 remove refl appThm trans 897 remove refl 709 remove appThm eqMp 734 remove appThm eqMp 750 remove appThm eqMp 758 remove appThm eqMp sym trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp 295 ref 296 ref 853 ref nil cons 899 def cons 297 ref 870 remove nil cons cons nil cons cons nil cons cons 534 ref subst proveHyp nil 209 ref 104 ref 853 remove appTerm nil cons cons 211 ref 866 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp nil "p" 102 remove var 899 remove cons nil cons nil cons cons 295 ref 79 ref cons 900 def 703 remove subst subst eqMp eqMp nil 209 ref 15 ref 864 ref appTerm nil cons cons 211 ref 865 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp 400 ref 391 ref 864 remove nil cons cons 761 remove cons nil cons cons 291 ref subst eqMp eqMp nil 209 ref 863 remove nil cons cons 211 ref 862 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp 400 ref 391 ref 861 remove nil cons cons 762 remove cons nil cons cons 291 ref subst eqMp eqMp nil 209 ref 860 remove nil cons cons 211 ref 859 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp 405 ref 404 ref 858 remove nil cons cons 764 ref cons nil cons cons 291 ref subst eqMp eqMp nil 209 ref 857 remove nil cons cons 211 ref 856 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp 405 ref 404 ref 855 remove nil cons cons 765 ref cons nil cons cons 291 ref subst eqMp eqMp subst appThm appThm absThm appThm absThm appThm trans absThm appThm trans absThm appThm trans absThm appThm 299 remove assume eqMp nil 209 ref 104 remove 105 remove 15 ref 306 ref 15 ref 334 ref 20 ref 347 ref 20 ref 348 ref 356 remove 33 ref 130 ref 131 ref 35 ref 311 ref appTerm 38 ref appTerm 901 def appTerm appTerm 131 ref 35 remove 339 ref appTerm 38 ref appTerm appTerm appTerm appTerm 902 def 110 remove 144 ref 45 ref 311 ref appTerm appTerm 121 ref 49 ref 311 ref appTerm 50 ref appTerm appTerm 340 ref 125 ref 52 ref 349 ref appTerm 53 ref appTerm appTerm 351 ref appTerm appTerm appTerm appTerm 144 ref 45 ref 339 ref appTerm appTerm 312 ref 123 ref 49 ref 339 ref appTerm 50 ref appTerm appTerm 350 ref 52 remove 351 ref appTerm 53 remove appTerm appTerm appTerm appTerm appTerm 144 ref 59 ref 339 ref appTerm 311 ref appTerm appTerm 121 ref 63 ref 311 ref appTerm 339 ref appTerm appTerm 340 remove 125 remove 66 ref 349 ref appTerm 351 ref appTerm appTerm 351 ref appTerm appTerm appTerm appTerm 312 remove 123 ref 63 ref 339 ref appTerm 311 ref appTerm appTerm 350 remove 66 remove 351 ref appTerm 349 ref appTerm appTerm appTerm appTerm appTerm appTerm appTerm 903 def appTerm appTerm 33 ref 901 remove appTerm 349 ref appTerm 351 ref appTerm 904 def appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 905 def appTerm 906 def nil cons cons 303 ref cons nil cons cons 273 ref subst proveHyp nil 296 ref "g" 100 remove var 907 def 212 ref 905 ref 907 ref varTerm 908 def appTerm 909 def appTerm 301 ref appTerm 910 def absTerm nil cons cons nil cons nil cons cons 900 remove 402 remove subst subst 907 remove nil 241 ref 910 remove nil cons cons nil cons nil cons cons 245 ref subst nil 209 ref 909 ref nil cons 911 def cons 303 ref cons nil cons cons 912 def 228 ref subst 912 remove 284 ref subst 909 ref betaConv 909 remove assume eqMp nil 209 ref 15 ref 306 remove 15 ref 334 ref 20 ref 347 remove 20 ref 348 remove 25 ref 908 ref 355 remove appTerm appTerm 902 remove 908 ref 903 remove appTerm appTerm 904 remove appTerm appTerm absTerm 913 def appTerm 914 def absTerm 915 def appTerm 916 def absTerm 917 def appTerm 918 def absTerm 919 def appTerm nil cons 920 def cons 921 def 303 remove cons nil cons cons 922 def 273 ref subst proveHyp 922 ref 228 ref subst 922 remove 284 ref subst 72 ref 16 ref 17 ref 21 ref 22 ref 908 ref 129 remove appTerm absTerm 923 def absTerm 924 def absTerm 925 def absTerm 926 def appTerm betaConv sym nil 391 ref 16 ref 15 ref 17 ref 20 ref 21 ref 20 ref 22 ref 25 ref 926 ref 27 ref appTerm 927 def 29 ref appTerm 30 ref appTerm 31 ref appTerm appTerm 41 ref 44 ref 47 ref 926 ref 51 ref appTerm 928 def 29 ref appTerm 54 ref appTerm 31 ref appTerm appTerm 56 ref 927 ref 57 ref appTerm 30 ref appTerm 58 ref appTerm appTerm 62 ref 926 ref 65 ref appTerm 929 def 29 ref appTerm 68 ref appTerm 31 ref appTerm appTerm 927 ref 70 ref appTerm 30 ref appTerm 71 ref appTerm appTerm appTerm appTerm appTerm appTerm appTerm 930 def absTerm 931 def appTerm 932 def absTerm 933 def appTerm 934 def absTerm 935 def appTerm 936 def absTerm nil cons cons nil cons nil cons cons 403 ref subst 16 ref nil 241 ref 936 remove nil cons cons nil cons nil cons cons 245 ref subst nil 391 ref 935 remove nil cons cons nil cons nil cons cons 403 remove subst 17 ref nil 241 ref 934 remove nil cons cons nil cons nil cons cons 245 ref subst nil 404 ref 933 remove nil cons cons nil cons nil cons cons 407 ref subst 21 ref nil 241 ref 932 remove nil cons cons nil cons nil cons cons 245 ref subst nil 404 ref 931 remove nil cons cons nil cons nil cons cons 407 remove subst 22 ref nil 241 ref 930 remove nil cons cons nil cons nil cons cons 245 ref subst 739 ref 927 remove betaConv 937 def 29 ref refl 938 def appThm 925 ref 29 ref appTerm betaConv trans 30 ref refl 939 def appThm 924 remove 30 ref appTerm betaConv trans 31 ref refl 940 def appThm 923 remove 31 ref appTerm betaConv trans appThm 41 ref refl 44 ref refl 941 def 47 ref refl 942 def 928 remove betaConv 938 ref appThm 17 ref 21 ref 22 ref 908 ref 146 ref 128 ref appTerm appTerm absTerm absTerm 943 def absTerm 29 ref appTerm betaConv trans 54 ref refl appThm 943 remove 54 ref appTerm betaConv trans 940 ref appThm 22 ref 908 ref 150 ref appTerm 944 def absTerm 31 ref appTerm betaConv trans appThm 56 ref refl 945 def 937 ref 57 ref refl appThm 925 ref 57 ref appTerm betaConv trans 939 ref appThm 21 ref 22 ref 908 ref 122 ref 152 remove 127 ref appTerm appTerm appTerm absTerm 946 def absTerm 30 ref appTerm betaConv trans 58 ref refl appThm 946 remove 58 ref appTerm betaConv trans appThm 62 ref refl 929 remove betaConv 938 ref appThm "v'" 1 remove var 947 def 21 ref 22 ref 908 ref 157 ref 123 ref 947 remove varTerm appTerm 127 ref appTerm appTerm appTerm absTerm absTerm absTerm 29 ref appTerm betaConv trans 68 ref refl appThm 21 ref 22 ref 908 ref 157 ref 128 remove appTerm appTerm absTerm absTerm 68 ref appTerm betaConv trans 940 ref appThm "x2'" 2 ref var 948 def 908 ref 157 remove 124 remove 158 remove 948 remove varTerm appTerm appTerm appTerm appTerm absTerm 31 ref appTerm betaConv trans appThm 937 remove 70 ref refl appThm 925 remove 70 ref appTerm betaConv trans 939 ref appThm 21 ref 22 ref 908 ref 122 ref 162 remove 127 remove appTerm appTerm appTerm absTerm 949 def absTerm 30 ref appTerm betaConv trans 71 ref refl appThm 949 remove 71 ref appTerm betaConv trans appThm appThm appThm appThm appThm appThm sym 739 ref nil 746 remove 748 remove 334 remove 732 remove cons 445 remove cons cons cons nil cons cons 913 ref 351 remove appTerm 950 def betaConv 915 ref 349 remove appTerm 951 def betaConv 917 ref 339 remove appTerm 952 def betaConv 919 ref 311 remove appTerm 953 def betaConv nil 921 remove 211 ref 953 remove nil cons cons nil cons cons nil cons cons 273 ref subst 400 ref 391 ref 919 remove nil cons cons 760 ref 361 remove cons nil cons cons nil cons cons 291 ref subst eqMp eqMp nil 209 ref 918 remove nil cons cons 211 ref 952 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp 400 remove 391 remove 917 remove nil cons cons 760 ref 360 remove cons nil cons cons nil cons cons 291 ref subst eqMp eqMp nil 209 ref 916 remove nil cons cons 211 ref 951 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp 405 ref 404 ref 915 remove nil cons cons 763 ref 359 remove cons nil cons cons nil cons cons 291 ref subst eqMp eqMp nil 209 ref 914 remove nil cons cons 211 ref 950 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp 405 remove 404 remove 913 remove nil cons cons 763 ref 358 remove cons nil cons cons nil cons cons 291 ref subst eqMp eqMp subst appThm 41 ref 44 ref 47 ref 944 ref appTerm 56 ref 908 ref 155 ref appTerm 954 def appTerm 62 ref 908 ref 161 ref appTerm 955 def appTerm 908 ref 164 ref appTerm 956 def appTerm 957 def appTerm 958 def appTerm 959 def appTerm 960 def appTerm 961 def refl appThm sym nil 209 ref 132 remove nil cons 962 def cons 963 def 211 ref 25 ref 33 ref 135 remove appTerm 908 ref 167 remove appTerm 964 def appTerm 174 remove appTerm appTerm 961 remove appTerm nil cons 965 def cons nil cons 966 def cons nil cons cons 967 def 228 ref subst 967 remove 284 ref subst 739 ref 357 ref 130 ref refl 968 def 131 ref refl 969 def nil 963 remove 211 ref 118 ref 39 ref appTerm "Data.Bool.F" const 12 ref constTerm 970 def appTerm nil cons cons nil cons cons nil cons cons 273 ref subst nil 250 ref 39 ref nil cons 971 def cons 972 def nil cons nil cons cons nil 209 ref 131 ref 254 ref appTerm 973 def nil cons 974 def cons 211 ref 118 ref 254 ref appTerm 970 ref appTerm nil cons 975 def cons nil cons cons nil cons cons 976 def 228 ref subst 976 remove 284 ref subst nil 209 ref 254 ref nil cons 977 def cons 211 ref 970 ref nil cons 978 def cons nil cons cons nil cons cons 596 remove subst 118 ref 973 ref appTerm refl 209 ref 214 ref 970 ref appTerm absTerm 979 def 254 ref appTerm betaConv appThm nil 237 ref 131 ref appTerm 979 remove appTerm axiom 263 ref appThm eqMp 973 remove assume eqMp nil 209 ref 212 ref 254 ref appTerm 980 def 970 ref appTerm nil cons cons 211 ref 212 ref 970 ref appTerm 254 ref appTerm nil cons cons nil cons cons nil cons cons 284 ref subst proveHyp nil 209 ref 978 ref cons 211 ref 977 ref cons nil cons cons nil cons cons 981 def 228 ref subst 981 remove 284 ref subst 209 ref 213 remove absTerm 982 def 254 ref appTerm 983 def betaConv nil 118 ref 970 ref appTerm 506 ref 982 ref appTerm 984 def appTerm axiom 970 ref assume eqMp nil 209 ref 984 remove nil cons cons 211 ref 983 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp 517 ref 510 ref 982 remove nil cons cons 559 ref 977 ref cons nil cons cons nil cons cons 291 ref subst eqMp eqMp eqMp nil 250 ref 978 remove cons 251 ref 977 remove cons nil cons cons nil cons cons 265 ref subst deductAntisym eqMp eqMp eqMp eqMp nil 250 ref 974 remove cons 251 ref 975 remove cons nil cons cons nil cons cons 265 ref subst deductAntisym eqMp 985 def subst eqMp 986 def appThm nil 118 ref 131 ref 970 ref appTerm appTerm 233 ref appTerm axiom 987 def trans appThm 134 ref refl 988 def appThm nil 241 ref 134 ref nil cons 989 def cons nil cons nil cons cons 990 def 241 ref 118 ref 130 ref 233 ref appTerm 243 ref appTerm appTerm 243 ref appTerm absTerm 991 def 243 ref appTerm 992 def betaConv nil 506 ref 991 ref appTerm 993 def axiom nil 209 ref 993 remove nil cons cons 211 ref 992 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp 517 ref 510 ref 991 remove nil cons cons 702 ref cons nil cons cons 291 ref subst eqMp eqMp subst trans appThm 964 ref refl 994 def appThm 357 ref 986 remove appThm 939 ref appThm 995 def 940 ref appThm nil "t2" 2 ref var 996 def 745 ref cons 997 def "t1" 2 remove var 998 def 747 ref cons nil cons 999 def cons nil cons cons 1000 def 406 ref "t2" 80 ref var 1001 def 448 ref 32 remove 0 ref 12 ref 0 remove 80 ref 190 remove nil cons cons opType nil cons cons opType constTerm 1002 def 970 ref appTerm "t1" 80 remove var 1003 def varTerm 1004 def appTerm 1001 ref varTerm 1005 def appTerm appTerm 1005 ref appTerm absTerm 1006 def 1005 ref appTerm 1007 def betaConv 1003 ref 201 ref 1006 ref appTerm 1008 def absTerm 1009 def 1004 ref appTerm 1010 def betaConv nil 201 ref 1009 ref appTerm 1011 def axiom nil 209 ref 1011 remove nil cons cons 211 ref 1010 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp 528 ref 277 ref 1009 remove nil cons cons 202 ref 1004 ref nil cons cons nil cons 1012 def cons nil cons cons 291 ref subst eqMp eqMp nil 209 ref 1008 remove nil cons cons 211 ref 1007 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp 528 ref 277 ref 1006 remove nil cons cons 202 remove 1005 ref nil cons cons nil cons 1013 def cons nil cons cons 291 ref subst eqMp eqMp 1014 def subst 1015 def subst trans appThm appThm 995 remove 960 ref refl appThm nil 996 ref 960 ref nil cons cons 999 ref cons nil cons cons 1015 ref subst trans appThm sym nil 209 ref 989 ref cons 1016 def 211 ref 25 ref 33 ref 134 remove appTerm 964 ref appTerm 31 ref appTerm appTerm 960 remove appTerm nil cons 1017 def cons nil cons 1018 def cons nil cons cons 1019 def 228 ref subst 1019 remove 284 ref subst 739 ref 357 ref 969 ref nil 1016 remove 211 ref 118 ref 43 ref appTerm 970 ref appTerm nil cons cons nil cons cons nil cons cons 273 ref subst nil 250 ref 43 ref nil cons 1020 def cons 1021 def nil cons nil cons cons 985 ref subst eqMp 1022 def appThm 987 remove trans appThm 994 remove appThm 940 ref appThm nil 997 ref 998 ref 964 ref nil cons cons nil cons cons nil cons cons 406 ref 1001 remove 448 ref 1002 remove 233 ref appTerm 1004 ref appTerm 1005 ref appTerm appTerm 1004 ref appTerm absTerm 1023 def 1005 remove appTerm 1024 def betaConv 1003 remove 201 ref 1023 ref appTerm 1025 def absTerm 1026 def 1004 remove appTerm 1027 def betaConv nil 201 remove 1026 ref appTerm 1028 def axiom nil 209 ref 1028 remove nil cons cons 211 ref 1027 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp 528 ref 277 ref 1026 remove nil cons cons 1012 remove cons nil cons cons 291 ref subst eqMp eqMp nil 209 ref 1025 remove nil cons cons 211 ref 1024 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp 528 remove 277 remove 1023 remove nil cons cons 1013 remove cons nil cons cons 291 ref subst eqMp eqMp 1029 def subst 1030 def subst trans appThm 357 ref 1022 remove appThm 940 ref appThm 959 ref refl appThm nil 996 ref 959 ref nil cons cons 998 ref 745 remove cons nil cons 1031 def cons nil cons cons 1015 ref subst trans appThm sym nil 209 ref 131 ref 46 ref appTerm nil cons 1032 def cons 1033 def 211 ref 25 ref 964 remove appTerm 959 remove appTerm nil cons 1034 def cons nil cons 1035 def cons nil cons cons 1036 def 228 ref subst 1036 remove 284 ref subst 739 ref 908 ref refl 1037 def 144 ref refl 1038 def nil 1033 remove 211 ref 118 ref 46 ref appTerm 970 ref appTerm nil cons cons nil cons cons nil cons cons 273 ref subst nil 250 ref 46 ref nil cons 1039 def cons 1040 def nil cons nil cons cons 985 ref subst eqMp 1041 def appThm 150 ref refl 1042 def appThm 166 ref refl 1043 def appThm nil "t2" 99 ref var 1044 def 166 ref nil cons cons "t1" 99 remove var 1045 def 150 remove nil cons cons nil cons cons nil cons cons 1046 def 187 remove nil cons 79 remove cons 1047 def 1014 remove subst 1048 def subst trans appThm appThm 357 ref 1041 remove appThm 944 ref refl 1049 def appThm 958 ref refl 1050 def appThm nil 996 ref 958 ref nil cons cons 998 ref 944 remove nil cons 1051 def cons nil cons cons nil cons cons 1052 def 1015 ref subst trans appThm sym nil 209 ref 131 ref 55 ref appTerm nil cons 1053 def cons 1054 def 211 ref 25 ref 908 ref 166 remove appTerm appTerm 958 remove appTerm nil cons 1055 def cons nil cons 1056 def cons nil cons cons 1057 def 228 ref subst 1057 remove 284 ref subst 739 ref 1037 ref 1038 ref nil 1054 remove 211 ref 118 ref 55 ref appTerm 970 ref appTerm nil cons cons nil cons cons nil cons cons 273 ref subst nil 250 ref 55 ref nil cons 1058 def cons 1059 def nil cons nil cons cons 985 ref subst eqMp 1060 def appThm 155 ref refl 1061 def appThm 165 ref refl 1062 def appThm nil 1044 ref 165 ref nil cons cons 1045 ref 155 remove nil cons cons nil cons cons nil cons cons 1063 def 1048 ref subst trans appThm appThm 357 ref 1060 remove appThm 954 ref refl 1064 def appThm 957 ref refl 1065 def appThm nil 996 ref 957 ref nil cons cons 998 ref 954 remove nil cons 1066 def cons nil cons cons nil cons cons 1067 def 1015 ref subst trans appThm sym nil 209 ref 131 ref 61 ref appTerm nil cons 1068 def cons 1069 def 211 ref 25 ref 908 ref 165 remove appTerm appTerm 957 remove appTerm nil cons 1070 def cons nil cons 1071 def cons nil cons cons 1072 def 228 ref subst 1072 remove 284 ref subst 739 ref 1037 ref 1038 ref nil 1069 remove 211 ref 118 ref 61 ref appTerm 970 ref appTerm nil cons cons nil cons cons nil cons cons 273 ref subst nil 250 ref 61 ref nil cons 1073 def cons 1074 def nil cons nil cons cons 985 remove subst eqMp 1075 def appThm 161 ref refl 1076 def appThm 164 ref refl 1077 def appThm nil 1044 remove 164 remove nil cons cons 1045 remove 161 remove nil cons cons nil cons cons nil cons cons 1078 def 1048 remove subst trans appThm appThm 357 ref 1075 remove appThm 955 ref refl 1079 def appThm 956 ref refl 1080 def appThm nil 996 ref 956 remove nil cons 1081 def cons 998 ref 955 remove nil cons 1082 def cons nil cons cons nil cons cons 1083 def 1015 ref subst trans appThm nil 763 ref 1081 remove cons nil cons nil cons cons 406 remove nil 241 ref 448 remove 206 ref appTerm 206 remove appTerm nil cons cons nil cons nil cons cons 245 ref subst 290 remove eqMp 1084 def subst 1085 def subst trans sym 244 ref eqMp eqMp nil 250 ref 1068 ref cons 251 ref 1070 ref cons nil cons 1086 def cons nil cons cons 265 ref subst deductAntisym eqMp nil 209 ref 1073 ref cons 1071 remove cons nil cons cons 1087 def 228 ref subst 1087 remove 284 ref subst 739 ref 1037 ref 1038 ref nil 241 ref 1073 ref cons nil cons nil cons cons 245 ref subst 61 ref assume eqMp 1088 def appThm 1076 remove appThm 1077 remove appThm 1078 remove 1047 remove 1029 remove subst 1089 def subst trans appThm appThm 357 ref 1088 remove appThm 1079 remove appThm 1080 remove appThm 1083 remove 1030 ref subst trans appThm nil 763 ref 1082 remove cons nil cons nil cons cons 1085 ref subst trans sym 244 ref eqMp eqMp nil 1074 ref 1086 remove cons nil cons cons 265 ref subst deductAntisym eqMp 241 ref "Data.Bool.\\/" const 117 remove constTerm 1090 def 243 ref appTerm 131 ref 243 ref appTerm appTerm absTerm 1091 def 61 remove appTerm 1092 def betaConv nil 506 ref 1091 ref appTerm 1093 def axiom 1094 def nil 209 ref 1093 remove nil cons cons 1095 def 211 ref 1092 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp 517 ref 510 ref 1091 ref nil cons cons 1096 def 559 ref 1073 remove cons nil cons cons nil cons cons 291 ref subst eqMp eqMp nil 1074 remove 251 ref 1068 remove cons "R" 12 ref var 1097 def 1070 remove cons nil cons cons cons nil cons cons nil 209 ref 212 ref 256 ref appTerm 1098 def 1097 ref varTerm 1099 def appTerm 1100 def nil cons cons 211 ref 1099 ref nil cons 1101 def cons nil cons cons nil cons cons 273 ref subst nil 209 ref 980 ref 1099 ref appTerm nil cons cons 211 ref 212 ref 1100 remove appTerm 1099 ref appTerm nil cons cons nil cons cons nil cons cons 273 ref subst "r" 12 remove var 1102 def 212 ref 980 remove 1102 ref varTerm 1103 def appTerm appTerm 1104 def 212 ref 1098 remove 1103 ref appTerm appTerm 1103 ref appTerm appTerm absTerm 1105 def 1099 remove appTerm 1106 def betaConv 118 ref 1090 ref 254 ref appTerm 1107 def 256 ref appTerm 1108 def appTerm refl 211 ref 506 ref 1102 ref 1104 remove 212 ref 585 remove 1103 ref appTerm appTerm 1103 ref appTerm 1109 def appTerm absTerm appTerm absTerm 256 remove appTerm betaConv appThm 237 remove 1107 remove appTerm refl 209 ref 211 ref 506 ref 1102 remove 212 ref 214 remove 1103 remove appTerm appTerm 1109 remove appTerm absTerm appTerm absTerm absTerm 1110 def 254 remove appTerm betaConv appThm nil 225 remove 1090 remove appTerm 1110 remove appTerm axiom 263 remove appThm eqMp 259 remove appThm eqMp 1108 remove assume eqMp nil 209 ref 506 ref 1105 ref appTerm nil cons cons 211 ref 1106 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp 517 ref 510 ref 1105 remove nil cons cons 559 ref 1101 remove cons nil cons cons nil cons cons 291 ref subst eqMp eqMp eqMp eqMp 1111 def subst proveHyp proveHyp proveHyp eqMp eqMp nil 250 ref 1053 ref cons 251 ref 1055 ref cons nil cons 1112 def cons nil cons cons 265 ref subst deductAntisym eqMp nil 209 ref 1058 ref cons 1056 remove cons nil cons cons 1113 def 228 ref subst 1113 remove 284 ref subst 739 ref 1037 ref 1038 ref nil 241 ref 1058 ref cons nil cons nil cons cons 245 ref subst 55 ref assume eqMp 1114 def appThm 1061 remove appThm 1062 remove appThm 1063 remove 1089 ref subst trans appThm appThm 357 ref 1114 remove appThm 1064 remove appThm 1065 remove appThm 1067 remove 1030 ref subst trans appThm nil 763 ref 1066 remove cons nil cons nil cons cons 1085 ref subst trans sym 244 ref eqMp eqMp nil 1059 ref 1112 remove cons nil cons cons 265 ref subst deductAntisym eqMp 1091 ref 55 remove appTerm 1115 def betaConv 1094 ref nil 1095 ref 211 ref 1115 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp 517 ref 1096 ref 559 ref 1058 remove cons nil cons cons nil cons cons 291 ref subst eqMp eqMp nil 1059 remove 251 ref 1053 remove cons 1097 ref 1055 remove cons nil cons cons cons nil cons cons 1111 ref subst proveHyp proveHyp proveHyp eqMp eqMp nil 250 ref 1032 ref cons 251 ref 1034 ref cons nil cons 1116 def cons nil cons cons 265 ref subst deductAntisym eqMp nil 209 ref 1039 ref cons 1035 remove cons nil cons cons 1117 def 228 ref subst 1117 remove 284 ref subst 739 ref 1037 ref 1038 ref nil 241 ref 1039 ref cons nil cons nil cons cons 245 remove subst 46 ref assume eqMp 1118 def appThm 1042 remove appThm 1043 remove appThm 1046 remove 1089 remove subst trans appThm appThm 357 ref 1118 remove appThm 1049 remove appThm 1050 remove appThm 1052 remove 1030 ref subst trans appThm nil 763 remove 1051 remove cons nil cons nil cons cons 1085 ref subst trans sym 244 ref eqMp eqMp nil 1040 ref 1116 remove cons nil cons cons 265 ref subst deductAntisym eqMp 1091 ref 46 remove appTerm 1119 def betaConv 1094 ref nil 1095 ref 211 ref 1119 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp 517 ref 1096 ref 559 ref 1039 remove cons nil cons cons nil cons cons 291 ref subst eqMp eqMp nil 1040 remove 251 ref 1032 remove cons 1097 ref 1034 remove cons nil cons cons cons nil cons cons 1111 ref subst proveHyp proveHyp proveHyp eqMp eqMp nil 250 ref 989 ref cons 251 ref 1017 ref cons nil cons 1120 def cons nil cons cons 265 ref subst deductAntisym eqMp nil 209 ref 1020 ref cons 1018 remove cons nil cons cons 1121 def 228 ref subst 1121 remove 284 ref subst 739 ref 357 ref 969 ref 713 ref 43 ref assume 1122 def appThm 38 ref refl 1123 def appThm nil 760 remove 38 ref nil cons cons nil cons nil cons cons 401 remove 1084 remove subst subst 1124 def trans 1125 def appThm nil 118 ref 131 remove 233 remove appTerm appTerm 970 ref appTerm axiom 1126 def trans appThm 1037 ref 145 ref refl 146 ref refl 123 ref refl 1127 def 1122 ref appThm 1128 def 148 ref refl appThm appThm 1129 def appThm 1038 ref 45 ref refl 1130 def 1122 ref appThm 1131 def appThm 122 ref refl 1132 def 1127 ref 49 ref refl 1133 def 1122 ref appThm 50 ref refl 1134 def appThm appThm 153 ref refl appThm appThm 1135 def appThm 1038 ref 59 ref refl 1122 ref appThm 27 ref refl 1136 def appThm 1137 def appThm 121 ref refl 1138 def 64 ref refl 1122 ref appThm appThm 1128 remove 159 ref refl appThm appThm 1139 def appThm 1132 remove 1127 ref 63 ref refl 1140 def 1122 remove appThm 1136 remove appThm appThm 163 ref refl 1141 def appThm appThm 1142 def appThm appThm appThm appThm appThm 940 ref appThm nil 997 remove 998 ref 908 ref 145 remove 146 remove 123 ref 38 ref appTerm 1143 def 148 remove appTerm appTerm 1144 def appTerm 144 ref 45 remove 38 ref appTerm 1145 def appTerm 1146 def 122 ref 123 ref 49 remove 38 ref appTerm 50 remove appTerm 1147 def appTerm 153 remove appTerm appTerm 1148 def appTerm 144 ref 59 remove 38 ref appTerm 27 ref appTerm 1149 def appTerm 121 ref 64 remove 38 ref appTerm appTerm 1143 remove 159 remove appTerm appTerm 1150 def appTerm 122 remove 123 ref 63 remove 38 ref appTerm 1151 def 27 ref appTerm appTerm 163 ref appTerm appTerm 1152 def appTerm appTerm appTerm appTerm nil cons cons nil cons cons nil cons cons 1015 ref subst trans appThm 357 ref 1125 remove appThm 940 ref appThm 942 remove 1037 ref 1129 remove appThm appThm 357 ref 1131 remove appThm 1037 ref 1135 remove appThm appThm 357 ref 1137 remove appThm 1037 ref 1139 remove appThm appThm 1037 ref 1142 remove appThm appThm appThm appThm appThm nil 996 ref 47 ref 908 ref 1144 remove appTerm appTerm 33 ref 1145 remove appTerm 1153 def 908 ref 1148 remove appTerm appTerm 33 ref 1149 remove appTerm 908 ref 1150 remove appTerm appTerm 908 ref 1152 remove appTerm appTerm appTerm appTerm nil cons cons 1031 remove cons nil cons cons 1030 ref subst trans appThm nil 765 remove nil cons cons 1085 ref subst trans sym 244 ref eqMp eqMp nil 1021 ref 1120 remove cons nil cons cons 265 ref subst deductAntisym eqMp 1091 ref 43 remove appTerm 1154 def betaConv 1094 ref nil 1095 ref 211 ref 1154 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp 517 ref 1096 ref 559 ref 1020 remove cons nil cons cons nil cons cons 291 ref subst eqMp eqMp nil 1021 remove 251 ref 989 remove cons 1097 ref 1017 remove cons nil cons cons cons nil cons cons 1111 ref subst proveHyp proveHyp proveHyp eqMp eqMp nil 250 ref 962 ref cons 251 ref 965 ref cons nil cons 1155 def cons nil cons cons 265 ref subst deductAntisym eqMp nil 209 ref 971 ref cons 966 remove cons nil cons cons 1156 def 228 remove subst 1156 remove 284 remove subst 739 remove 357 ref 968 remove 969 remove 713 remove 39 ref assume 1157 def appThm 1123 remove appThm 1124 remove trans 1158 def appThm 1126 remove trans appThm 988 remove appThm 990 remove 241 remove 118 remove 130 remove 970 ref appTerm 243 ref appTerm appTerm 970 remove appTerm absTerm 1159 def 243 remove appTerm 1160 def betaConv nil 506 remove 1159 ref appTerm 1161 def axiom nil 209 ref 1161 remove nil cons cons 211 ref 1160 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp 517 ref 510 remove 1159 remove nil cons cons 702 remove cons nil cons cons 291 ref subst eqMp eqMp subst trans appThm 1037 ref 1038 ref 1130 remove 1157 ref appThm 1162 def appThm 1138 ref 1133 remove 1157 ref appThm 1134 remove appThm appThm 149 ref refl appThm 1163 def appThm 151 ref refl 1138 ref 1157 ref appThm 1164 def 154 ref refl appThm 1165 def appThm 1038 remove 60 ref refl 1157 ref appThm 1166 def appThm 1138 remove 1140 remove 1157 ref appThm 938 remove appThm appThm 160 ref refl appThm 1167 def appThm 1164 remove 1127 remove 69 ref refl 1157 remove appThm appThm 1141 remove appThm appThm 1168 def appThm appThm appThm appThm appThm 357 ref 1158 remove appThm 939 remove appThm 1169 def 940 remove appThm 1000 remove 1030 ref subst trans appThm nil 996 ref 747 remove cons 998 remove 908 ref 1146 remove 121 ref 1147 remove appTerm 149 remove appTerm 1170 def appTerm 151 remove 121 ref 38 ref appTerm 1171 def 154 remove appTerm 1172 def appTerm 144 remove 60 remove 38 ref appTerm 1173 def appTerm 121 remove 1151 remove 29 ref appTerm appTerm 160 remove appTerm 1174 def appTerm 1171 remove 123 remove 69 remove 38 remove appTerm appTerm 163 remove appTerm appTerm 1175 def appTerm appTerm appTerm appTerm nil cons cons nil cons cons nil cons cons 1015 remove subst trans appThm 1169 remove 941 remove 357 ref 1162 remove appThm 1037 ref 1163 remove appThm appThm 945 remove 1037 ref 1165 remove appThm appThm 357 remove 1166 remove appThm 1037 ref 1167 remove appThm appThm 1037 remove 1168 remove appThm appThm appThm appThm appThm appThm nil 996 remove 44 ref 1153 remove 908 ref 1170 remove appTerm appTerm 56 ref 908 ref 1172 remove appTerm appTerm 33 remove 1173 remove appTerm 908 ref 1174 remove appTerm appTerm 908 remove 1175 remove appTerm appTerm appTerm appTerm appTerm nil cons cons 999 remove cons nil cons cons 1030 remove subst trans appThm nil 764 remove nil cons cons 1085 remove subst trans sym 244 remove eqMp eqMp nil 972 ref 1155 remove cons nil cons cons 265 ref subst deductAntisym eqMp 1091 remove 39 remove appTerm 1176 def betaConv 1094 remove nil 1095 remove 211 ref 1176 remove nil cons cons nil cons cons nil cons cons 273 ref subst proveHyp 517 remove 1096 remove 559 remove 971 remove cons nil cons cons nil cons cons 291 remove subst eqMp eqMp nil 972 remove 251 ref 962 remove cons 1097 remove 965 remove cons nil cons cons cons nil cons cons 1111 remove subst proveHyp proveHyp proveHyp eqMp eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp 78 remove "P" 74 remove var 72 remove nil cons cons "x" 9 ref var 926 remove nil cons cons nil cons cons nil cons cons 534 remove subst proveHyp eqMp nil 250 ref 920 remove cons 251 remove 302 remove cons nil cons 1177 def cons nil cons cons 265 ref subst deductAntisym eqMp eqMp eqMp nil 250 ref 911 remove cons 1177 ref cons nil cons cons 265 ref subst deductAntisym eqMp eqMp absThm eqMp nil 209 remove 178 remove 297 ref 212 ref 905 ref 297 remove varTerm appTerm appTerm 301 ref appTerm absTerm appTerm nil cons cons 211 remove 212 remove 906 remove appTerm 301 remove appTerm nil cons cons nil cons cons nil cons cons 273 remove subst proveHyp 295 remove 296 remove 905 remove nil cons cons 1177 ref cons nil cons cons 560 remove subst eqMp eqMp eqMp nil 250 remove 300 remove cons 1177 remove cons nil cons cons 265 remove subst deductAntisym eqMp eqMp eqMp eqMp defineConstList 1178 def pop 1179 def pop 1178 remove nil 15 ref 16 remove 15 remove 17 remove 20 ref 21 remove 20 remove 22 remove 25 remove 1179 remove hdTl pop 9 remove constTerm 1180 def 27 remove appTerm 1181 def 29 ref appTerm 30 ref appTerm 31 ref appTerm appTerm 41 remove 44 remove 47 remove 1180 ref 51 remove appTerm 29 ref appTerm 54 remove appTerm 31 ref appTerm appTerm 56 remove 1181 ref 57 remove appTerm 30 ref appTerm 58 remove appTerm appTerm 62 remove 1180 remove 65 remove appTerm 29 remove appTerm 68 remove appTerm 31 remove appTerm appTerm 1181 remove 70 remove appTerm 30 remove appTerm 71 remove appTerm appTerm appTerm appTerm appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm thm