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