path: "vendor/opentheory/data/theories/natural-fibonacci-exists/natural-fibonacci-exists.art"
6 version "Data.Bool.!" const 0 def "->" typeOp 1 def 1 ref 1 ref "Number.Natural.natural" typeOp nil opType 2 def "bool" typeOp nil opType 3 def nil cons 4 def cons opType 5 def 4 ref cons opType 6 def 4 ref cons opType constTerm 7 def refl "p" 5 ref var 8 def "Data.Bool.==>" const 1 ref 3 ref 1 ref 3 ref 4 ref cons opType 9 def nil cons 10 def cons opType 11 def constTerm 12 def refl 13 def "Data.Bool./\\" const 11 ref constTerm 14 def 8 ref varTerm 15 def "Number.Natural.zero" const 2 ref constTerm 16 def appTerm 17 def appTerm 18 def refl 14 ref refl 19 def 15 ref refl 20 def nil "n" 2 ref var 21 def 16 ref nil cons 22 def cons 23 def nil cons nil cons cons 24 def 21 ref "=" const 25 def 1 ref 2 ref 5 ref nil cons 26 def cons opType 27 def constTerm 28 def "Number.Natural.bit1" const 1 ref 2 ref 2 ref nil cons 29 def cons opType 30 def constTerm 31 def 21 ref varTerm 32 def appTerm 33 def appTerm "Number.Natural.suc" const 30 ref constTerm 34 def "Number.Natural.bit0" const 30 ref constTerm 35 def 32 ref appTerm 36 def appTerm 37 def appTerm absTerm 38 def 32 ref appTerm 39 def betaConv nil 0 ref 6 ref constTerm 40 def 38 ref appTerm 41 def axiom nil "p" 3 ref var 42 def 41 remove nil cons cons "q" 3 ref var 43 def 39 remove nil cons cons nil cons cons nil cons cons 25 ref 11 ref constTerm 44 def 12 ref 42 ref varTerm 45 def appTerm 46 def 43 ref varTerm 47 def appTerm 48 def appTerm 49 def refl 42 ref 43 ref 44 ref 14 ref 45 ref appTerm 50 def 47 ref appTerm 51 def appTerm 52 def 45 ref appTerm absTerm 53 def absTerm 54 def 45 ref appTerm betaConv 47 ref refl 55 def appThm 53 remove 47 ref appTerm betaConv trans appThm nil 25 ref 1 ref 11 ref 1 ref 11 ref 4 ref cons opType 56 def nil cons cons opType constTerm 57 def 12 ref appTerm 54 remove appTerm axiom 45 ref refl 58 def appThm 55 ref appThm eqMp 59 def sym 60 def 52 remove refl 43 ref 25 ref 1 ref 56 ref 1 ref 56 remove 4 ref cons opType nil cons cons opType constTerm 61 def "f" 11 ref var 62 def 62 ref varTerm 63 def 45 ref appTerm 47 ref appTerm absTerm 64 def appTerm 62 ref 63 ref "Data.Bool.T" const 3 ref constTerm 65 def appTerm 65 ref appTerm absTerm 66 def appTerm absTerm 67 def 47 ref appTerm betaConv appThm 25 ref 1 ref 9 ref 1 ref 9 ref 4 ref cons opType 68 def nil cons cons opType constTerm 69 def 50 ref appTerm refl 42 ref 67 remove absTerm 70 def 45 ref appTerm betaConv appThm nil 57 ref 14 ref appTerm 70 ref appTerm axiom 71 def 58 remove appThm eqMp 55 ref appThm eqMp 72 def sym 62 ref 63 ref refl nil "t" 3 ref var 73 def 45 ref nil cons 74 def cons nil cons nil cons cons 75 def 44 ref 73 ref varTerm 76 def appTerm 77 def 65 ref appTerm 78 def assume sym nil 65 ref axiom 79 def eqMp 76 ref assume 79 ref deductAntisym deductAntisym 80 def subst 45 ref assume 81 def eqMp appThm nil 73 ref 47 ref nil cons 82 def cons nil cons nil cons cons 83 def 80 ref subst 47 ref assume eqMp appThm absThm eqMp 84 def nil "P" 3 ref var 85 def 74 ref cons "Q" 3 ref var 86 def 82 ref cons nil cons cons nil cons cons 44 ref refl 87 def 62 ref 63 remove 85 ref varTerm 88 def appTerm 89 def 86 ref varTerm 90 def appTerm absTerm 91 def 42 ref 43 ref 45 ref absTerm absTerm 92 def appTerm betaConv 92 ref 88 ref appTerm betaConv 90 ref refl 93 def appThm 43 ref 88 ref absTerm 90 ref appTerm betaConv trans trans appThm 66 ref 92 ref appTerm betaConv 92 ref 65 ref appTerm betaConv 65 ref refl 94 def appThm 43 ref 65 ref absTerm 65 ref appTerm betaConv trans trans appThm 44 ref 14 ref 88 ref appTerm 95 def 90 ref appTerm 96 def appTerm refl 43 ref 61 remove 62 remove 89 remove 47 ref appTerm absTerm appTerm 66 ref appTerm absTerm 90 ref appTerm betaConv appThm 69 ref 95 remove appTerm refl 70 remove 88 ref appTerm betaConv appThm 71 remove 88 ref refl 97 def appThm eqMp 93 ref appThm eqMp 96 remove assume eqMp 98 def 92 remove refl appThm eqMp sym 79 ref eqMp 99 def subst 100 def deductAntisym eqMp 59 remove 48 ref assume eqMp sym 81 ref eqMp 87 ref 64 remove 42 ref 43 ref 47 ref absTerm 101 def absTerm 102 def appTerm betaConv 102 ref 45 ref appTerm betaConv 55 ref appThm 101 ref 47 ref appTerm betaConv trans trans appThm 66 remove 102 ref appTerm betaConv 102 ref 65 ref appTerm betaConv 94 remove appThm 101 ref 65 ref appTerm betaConv trans trans 103 def appThm 72 remove 51 remove assume eqMp 102 ref refl 104 def appThm eqMp sym 79 ref eqMp 105 def proveHyp deductAntisym 106 def subst proveHyp "A" 29 ref cons 107 def nil cons 108 def "P" 5 ref var 109 def 38 remove nil cons cons "x" 2 ref var 110 def 32 ref nil cons 111 def cons nil cons 112 def cons nil cons cons nil 42 ref 0 ref 1 ref 1 ref "A" varType 113 def 4 ref cons opType 114 def 4 ref cons opType 115 def constTerm 116 def "P" 114 ref var 117 def varTerm 118 def appTerm 119 def nil cons 120 def cons 43 ref 118 ref "x" 113 ref var 121 def varTerm 122 def appTerm 123 def nil cons 124 def cons nil cons cons nil cons cons 125 def 60 ref subst 125 remove 105 remove 84 remove deductAntisym 126 def subst 44 ref 123 ref appTerm refl 121 ref 65 ref absTerm 127 def 122 ref appTerm betaConv appThm "p" 114 ref var 128 def 25 ref 1 ref 114 ref 115 ref nil cons cons opType constTerm 128 ref varTerm 129 def appTerm 127 remove appTerm absTerm 130 def 118 ref appTerm betaConv 131 def nil 25 ref 1 ref 115 ref 1 ref 115 ref 4 ref cons opType 132 def nil cons cons opType constTerm 133 def 116 ref appTerm 130 remove appTerm axiom 118 ref refl 134 def appThm 135 def 119 ref assume eqMp eqMp 122 ref refl 136 def appThm eqMp sym 79 ref eqMp eqMp nil 85 ref 120 remove cons 86 ref 124 ref cons nil cons cons nil cons cons 99 ref subst deductAntisym eqMp 137 def subst eqMp eqMp 138 def subst 34 ref refl 139 def nil 28 ref 35 ref 16 ref appTerm appTerm 140 def 16 ref appTerm axiom 141 def appThm 142 def trans 143 def appThm appThm 40 ref refl 144 def 21 ref 13 ref 14 ref 15 ref 32 ref appTerm 145 def appTerm 146 def refl 20 ref "Number.Natural.+" const 1 ref 2 ref 30 ref nil cons 147 def cons opType 148 def constTerm 149 def 32 ref appTerm 150 def refl 151 def 143 ref appThm nil 23 ref "m" 2 ref var 152 def 111 ref cons 153 def nil cons 154 def cons nil cons cons 21 ref 28 ref 149 ref 152 ref varTerm 155 def appTerm 156 def 34 ref 32 ref appTerm 157 def appTerm appTerm 34 ref 156 ref 32 ref appTerm 158 def appTerm 159 def appTerm absTerm 160 def 32 ref appTerm 161 def betaConv 152 ref 40 ref 160 ref appTerm 162 def absTerm 163 def 155 ref appTerm 164 def betaConv nil 40 ref 163 ref appTerm 165 def axiom nil 42 ref 165 remove nil cons cons 43 ref 164 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 163 remove nil cons cons 110 ref 155 ref nil cons 166 def cons nil cons 167 def cons nil cons cons 137 ref subst eqMp eqMp nil 42 ref 162 remove nil cons cons 43 ref 161 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 160 remove nil cons cons 112 ref cons nil cons cons 137 ref subst eqMp eqMp 168 def subst 139 ref nil 154 ref nil cons cons 169 def 152 ref 28 ref 156 ref 16 ref appTerm appTerm 155 ref appTerm absTerm 170 def 155 ref appTerm 171 def betaConv nil 40 ref 170 ref appTerm 172 def axiom nil 42 ref 172 remove nil cons cons 43 ref 171 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 170 remove nil cons cons 167 ref cons nil cons cons 137 ref subst eqMp eqMp 173 def subst appThm trans 174 def trans appThm appThm appThm 20 remove 151 ref 35 ref refl 175 def 143 ref appThm 24 ref 21 ref 28 ref 35 ref 157 ref appTerm 176 def appTerm 177 def 34 ref 37 ref appTerm appTerm absTerm 178 def 32 ref appTerm 179 def betaConv nil 40 ref 178 ref appTerm 180 def axiom nil 42 ref 180 remove nil cons cons 43 ref 179 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 178 remove nil cons cons 112 ref cons nil cons cons 137 ref subst eqMp eqMp 181 def subst 139 ref 142 remove appThm trans trans 182 def appThm nil 21 ref 34 ref 16 ref appTerm 183 def nil cons 184 def cons 154 ref cons nil cons cons 168 ref subst 139 ref 174 remove appThm trans trans 185 def appThm appThm absThm appThm appThm appThm appThm 40 ref 21 ref 145 ref absTerm 186 def appTerm 187 def refl appThm absThm appThm sym nil "P" 6 ref var 188 def 8 ref 12 ref 18 ref 14 ref 15 ref 183 ref appTerm 189 def appTerm 40 ref 21 ref 12 ref 146 ref 15 ref 157 ref appTerm 190 def appTerm appTerm 15 ref 34 ref 157 ref appTerm appTerm appTerm absTerm 191 def appTerm 192 def appTerm 193 def appTerm 194 def appTerm 187 ref appTerm 195 def absTerm nil cons cons nil cons nil cons cons "A" 26 remove cons nil cons 196 def nil nil cons 197 def cons 44 ref 119 remove appTerm refl 131 remove appThm 135 remove eqMp sym 198 def subst subst 8 ref nil 73 ref 195 remove nil cons cons nil cons nil cons cons 80 ref subst nil 42 ref 194 remove nil cons 199 def cons 43 ref 187 ref nil cons 200 def cons nil cons cons nil cons cons 201 def 60 ref subst 201 remove 126 ref subst nil 85 ref 17 ref nil cons cons 86 ref 193 remove nil cons cons nil cons cons nil cons cons 202 def 99 ref subst 202 remove 87 ref 91 remove 102 ref appTerm betaConv 102 remove 88 ref appTerm betaConv 93 ref appThm 101 remove 90 ref appTerm betaConv trans trans appThm 103 remove appThm 98 remove 104 remove appThm eqMp sym 79 ref eqMp 203 def subst nil 85 ref 189 ref nil cons cons 86 ref 192 remove nil cons 204 def cons nil cons cons nil cons cons 205 def 99 ref subst 205 remove 203 ref subst nil 109 ref 186 remove nil cons cons nil cons nil cons cons 108 ref 197 ref cons 206 def 198 ref subst 207 def subst 21 ref nil 73 ref 145 ref nil cons 208 def cons nil cons nil cons cons 80 ref subst nil 109 ref 21 ref 12 ref 40 ref 152 ref 12 ref "Number.Natural.<" const 27 ref constTerm 209 def 155 ref appTerm 210 def 32 ref appTerm 211 def appTerm 212 def 40 ref 21 ref 12 ref 28 ref 155 ref appTerm 213 def 32 ref appTerm 214 def appTerm 145 ref appTerm absTerm 215 def appTerm 216 def appTerm absTerm appTerm appTerm 145 ref appTerm 217 def absTerm 218 def nil cons cons nil cons nil cons cons 207 ref subst 21 ref nil 73 ref 217 remove nil cons cons nil cons nil cons cons 80 ref subst 13 ref 87 ref 144 ref 152 ref 13 ref 152 ref 211 ref absTerm 219 def 155 ref appTerm betaConv appThm 220 def 144 ref 21 ref 152 ref 215 ref absTerm 221 def 155 ref appTerm betaConv 222 def 32 ref refl 223 def appThm 215 ref 32 ref appTerm betaConv trans absThm appThm appThm absThm appThm appThm 144 ref "n'" 2 ref var 224 def 144 ref 152 ref 220 ref 222 remove 224 ref varTerm 225 def refl appThm 215 remove 225 ref appTerm betaConv trans appThm absThm appThm absThm appThm appThm nil 109 ref 219 ref nil cons cons 226 def "Q" 27 ref var 227 def 221 remove nil cons cons nil cons cons nil cons cons "B" 29 remove cons 108 ref cons 197 ref cons nil 42 ref 44 ref 116 ref 121 ref 12 ref 123 ref appTerm 228 def 0 ref 1 ref 1 ref "B" varType 229 def 4 ref cons opType 230 def 4 ref cons opType 231 def constTerm 232 def "y" 229 ref var 233 def "Q" 1 ref 113 ref 230 ref nil cons 234 def cons opType 235 def var varTerm 236 def 122 ref appTerm 237 def 233 ref varTerm 238 def appTerm 239 def absTerm 240 def appTerm 241 def appTerm absTerm 242 def appTerm 243 def appTerm 232 ref 233 ref 116 ref 121 ref 228 ref 239 ref appTerm absTerm 244 def appTerm absTerm 245 def appTerm 246 def appTerm 247 def nil cons cons nil cons nil cons cons 44 ref 45 ref appTerm 248 def refl 249 def nil 73 ref "Data.Bool.~" const 9 ref constTerm 250 def 45 ref appTerm 251 def nil cons 252 def cons nil cons nil cons cons 73 ref 44 ref 12 ref 76 ref appTerm 253 def "Data.Bool.F" const 3 ref constTerm 254 def appTerm appTerm 250 ref 76 ref appTerm 255 def appTerm absTerm 256 def 76 ref appTerm 257 def betaConv nil 0 ref 68 ref constTerm 258 def 256 ref appTerm 259 def axiom nil 42 ref 259 remove nil cons cons 43 ref 257 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp "A" 4 ref cons nil cons 260 def "P" 9 ref var 261 def 256 remove nil cons cons "x" 3 ref var 262 def 76 ref nil cons 263 def cons nil cons 264 def cons nil cons cons 137 ref subst eqMp eqMp 265 def subst appThm sym 249 remove 75 ref 73 ref 44 ref 250 ref 255 ref appTerm appTerm 76 ref appTerm absTerm 266 def 76 ref appTerm 267 def betaConv nil 258 ref 266 ref appTerm 268 def axiom nil 42 ref 268 remove nil cons cons 43 ref 267 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 260 ref 261 ref 266 remove nil cons cons 264 ref cons nil cons cons 137 ref subst eqMp eqMp 269 def subst 270 def appThm nil 262 ref 74 ref cons nil cons 271 def nil cons cons 260 ref 197 ref cons 272 def nil 73 ref 25 ref 1 ref 113 ref 114 ref nil cons 273 def cons opType 274 def constTerm 275 def 122 ref appTerm 122 ref appTerm nil cons cons nil cons nil cons cons 80 ref subst 136 ref eqMp 276 def subst 277 def subst trans sym 79 ref eqMp eqMp 278 def subst sym nil 42 ref 250 ref 247 remove appTerm 279 def nil cons 280 def cons 43 ref 254 ref nil cons 281 def cons nil cons 282 def cons nil cons cons 283 def 60 ref subst 283 remove 126 ref subst nil 42 ref 243 remove nil cons cons 43 ref 246 remove nil cons cons nil cons cons nil cons cons nil 42 ref 248 ref 254 ref appTerm 284 def nil cons 285 def cons 286 def 43 ref 44 ref 250 ref 248 ref 47 ref appTerm 287 def appTerm appTerm "Data.Bool.\\/" const 11 remove constTerm 288 def 50 ref 250 ref 47 ref appTerm 289 def appTerm 290 def appTerm 14 ref 251 ref appTerm 47 ref appTerm appTerm appTerm nil cons 291 def cons nil cons 292 def cons nil cons cons 293 def 60 ref subst 293 remove 126 ref subst 44 ref "_550" 3 ref var 294 def 44 ref 250 ref 44 ref 294 remove varTerm 295 def appTerm 47 ref appTerm appTerm appTerm 288 ref 14 ref 295 ref appTerm 289 ref appTerm appTerm 14 ref 250 ref 295 remove appTerm appTerm 47 ref appTerm appTerm appTerm absTerm 296 def 45 ref appTerm 297 def appTerm refl 298 def 296 ref 254 ref appTerm betaConv appThm 87 ref 297 remove betaConv appThm 299 def 44 ref 250 ref 44 ref 254 ref appTerm 300 def 47 ref appTerm appTerm appTerm 288 ref 14 ref 254 ref appTerm 301 def 289 ref appTerm 302 def appTerm 14 ref 250 ref 254 ref appTerm 303 def appTerm 47 ref appTerm appTerm appTerm refl appThm trans 296 remove refl 304 def 284 remove assume 305 def appThm eqMp sym 87 ref 250 ref refl 306 def 83 ref 73 ref 44 ref 300 remove 76 ref appTerm appTerm 255 ref appTerm absTerm 307 def 76 ref appTerm 308 def betaConv nil 258 ref 307 ref appTerm 309 def axiom nil 42 ref 309 remove nil cons cons 43 ref 308 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 260 ref 261 ref 307 remove nil cons cons 264 ref cons nil cons cons 137 ref subst eqMp eqMp 310 def subst appThm 83 ref 269 ref subst trans appThm 288 ref refl 311 def nil 73 ref 289 ref nil cons 312 def cons nil cons nil cons cons 313 def 73 ref 44 ref 301 ref 76 ref appTerm appTerm 254 ref appTerm absTerm 314 def 76 ref appTerm 315 def betaConv nil 258 ref 314 ref appTerm 316 def axiom nil 42 ref 316 remove nil cons cons 43 ref 315 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 260 ref 261 ref 314 remove nil cons cons 264 ref cons nil cons cons 137 ref subst eqMp eqMp 317 def subst 318 def appThm 19 ref nil 44 ref 303 ref appTerm 65 ref appTerm axiom 319 def appThm 55 ref appThm 83 ref 73 ref 44 ref 14 ref 65 ref appTerm 320 def 76 ref appTerm appTerm 76 ref appTerm absTerm 321 def 76 ref appTerm 322 def betaConv nil 258 ref 321 ref appTerm 323 def axiom nil 42 ref 323 remove nil cons cons 43 ref 322 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 260 ref 261 ref 321 remove nil cons cons 264 ref cons nil cons cons 137 ref subst eqMp eqMp 324 def subst trans appThm 83 ref 73 ref 44 ref 288 ref 254 ref appTerm 325 def 76 ref appTerm appTerm 76 ref appTerm absTerm 326 def 76 ref appTerm 327 def betaConv nil 258 ref 326 ref appTerm 328 def axiom nil 42 ref 328 remove nil cons cons 43 ref 327 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 260 ref 261 ref 326 remove nil cons cons 264 ref cons nil cons cons 137 ref subst eqMp eqMp 329 def subst 330 def trans appThm nil 262 ref 82 ref cons nil cons 331 def nil cons cons 277 ref subst 332 def trans sym 79 ref eqMp eqMp eqMp nil 85 ref 285 ref cons 333 def 86 ref 291 ref cons nil cons 334 def cons nil cons cons 99 ref subst deductAntisym eqMp nil 42 ref 248 remove 65 ref appTerm 335 def nil cons 336 def cons 337 def 292 remove cons nil cons cons 338 def 60 ref subst 338 remove 126 ref subst 298 remove "_548" 3 ref var 339 def 44 ref 250 ref 44 ref 339 remove varTerm 340 def appTerm 47 ref appTerm appTerm appTerm 288 ref 14 ref 340 ref appTerm 289 ref appTerm appTerm 14 ref 250 ref 340 remove appTerm appTerm 47 ref appTerm appTerm appTerm absTerm 65 ref appTerm betaConv appThm 299 remove 44 ref 250 ref 44 ref 65 ref appTerm 341 def 47 ref appTerm appTerm appTerm 288 ref 320 ref 289 ref appTerm 342 def appTerm 14 ref 250 ref 65 ref appTerm 343 def appTerm 47 ref appTerm appTerm appTerm refl appThm trans 304 remove 335 remove assume 344 def appThm eqMp sym 87 ref 306 ref 83 ref 73 ref 44 ref 341 remove 76 ref appTerm appTerm 76 ref appTerm absTerm 345 def 76 ref appTerm 346 def betaConv nil 258 ref 345 ref appTerm 347 def axiom nil 42 ref 347 remove nil cons cons 43 ref 346 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 260 ref 261 ref 345 remove nil cons cons 264 ref cons nil cons cons 137 ref subst eqMp eqMp 348 def subst appThm appThm 311 ref 313 ref 324 ref subst 349 def appThm 19 ref nil 44 ref 343 ref appTerm 254 ref appTerm axiom 350 def appThm 55 ref appThm 83 ref 317 ref subst trans appThm 313 remove 73 ref 44 ref 288 ref 76 ref appTerm 254 ref appTerm appTerm 76 ref appTerm absTerm 351 def 76 ref appTerm 352 def betaConv nil 258 ref 351 ref appTerm 353 def axiom nil 42 ref 353 remove nil cons cons 43 ref 352 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 260 ref 261 ref 351 remove nil cons cons 264 ref cons nil cons cons 137 ref subst eqMp eqMp subst trans appThm nil 262 ref 312 remove cons nil cons nil cons cons 277 ref subst 354 def trans sym 79 ref eqMp eqMp eqMp nil 85 ref 336 remove cons 355 def 334 remove cons nil cons cons 99 ref subst deductAntisym eqMp 73 ref 288 ref 78 ref appTerm 77 remove 254 ref appTerm 356 def appTerm absTerm 357 def 45 ref appTerm 358 def betaConv nil 258 ref 357 ref appTerm 359 def axiom 360 def nil 42 ref 359 remove nil cons cons 361 def 43 ref 358 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 260 ref 261 ref 357 ref nil cons cons 362 def 271 ref cons nil cons cons 137 ref subst eqMp eqMp 363 def nil 355 ref 86 ref 285 remove cons 364 def "R" 3 ref var 365 def 291 remove cons nil cons cons cons nil cons cons nil 42 ref 12 ref 90 ref appTerm 366 def 365 ref varTerm 367 def appTerm 368 def nil cons cons 43 ref 367 ref nil cons 369 def cons nil cons cons nil cons cons 106 ref subst nil 42 ref 12 ref 88 ref appTerm 370 def 367 ref appTerm nil cons cons 43 ref 12 ref 368 remove appTerm 367 ref appTerm nil cons cons nil cons cons nil cons cons 106 ref subst "r" 3 ref var 371 def 12 ref 370 ref 371 ref varTerm 372 def appTerm appTerm 373 def 12 ref 366 ref 372 ref appTerm appTerm 372 ref appTerm appTerm absTerm 374 def 367 remove appTerm 375 def betaConv 44 ref 288 ref 88 ref appTerm 376 def 90 ref appTerm 377 def appTerm refl 43 ref 258 ref 371 ref 373 remove 12 ref 12 ref 47 ref appTerm 372 ref appTerm appTerm 372 ref appTerm 378 def appTerm absTerm appTerm absTerm 90 ref appTerm betaConv appThm 69 remove 376 remove appTerm refl 42 ref 43 ref 258 ref 371 remove 12 ref 46 remove 372 remove appTerm appTerm 378 remove appTerm absTerm appTerm absTerm absTerm 379 def 88 ref appTerm betaConv appThm nil 57 remove 288 ref appTerm 379 remove appTerm axiom 97 remove appThm eqMp 93 remove appThm eqMp 380 def 377 remove assume eqMp nil 42 ref 258 ref 374 ref appTerm nil cons cons 43 ref 375 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 260 ref 261 ref 374 remove nil cons cons 262 ref 369 remove cons nil cons cons nil cons cons 137 ref subst eqMp eqMp eqMp eqMp 381 def subst proveHyp proveHyp proveHyp 382 def subst 311 ref 19 ref 116 ref refl 383 def 121 ref nil 42 ref 124 ref cons 384 def 43 ref 241 ref nil cons cons nil cons cons nil cons cons 385 def nil 286 ref 43 ref 49 remove 288 ref 251 ref appTerm 47 ref appTerm appTerm nil cons 386 def cons nil cons 387 def cons nil cons cons 388 def 60 ref subst 388 remove 126 ref subst 44 ref "_538" 3 ref var 389 def 44 ref 12 ref 389 remove varTerm 390 def appTerm 47 ref appTerm appTerm 288 ref 250 ref 390 remove appTerm appTerm 47 ref appTerm appTerm absTerm 391 def 45 ref appTerm 392 def appTerm refl 393 def 391 ref 254 ref appTerm betaConv appThm 87 ref 392 remove betaConv appThm 394 def 44 ref 12 ref 254 ref appTerm 395 def 47 ref appTerm 396 def appTerm 288 ref 303 remove appTerm 397 def 47 ref appTerm appTerm refl appThm trans 391 remove refl 398 def 305 ref appThm eqMp sym 87 ref 83 ref 73 ref 44 ref 395 remove 76 ref appTerm appTerm 65 ref appTerm absTerm 399 def 76 ref appTerm 400 def betaConv nil 258 ref 399 ref appTerm 401 def axiom nil 42 ref 401 remove nil cons cons 43 ref 400 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 260 ref 261 ref 399 remove nil cons cons 264 ref cons nil cons cons 137 ref subst eqMp eqMp subst 402 def appThm 311 ref 319 ref appThm 403 def 55 ref appThm 83 ref 73 ref 44 ref 288 ref 65 ref appTerm 404 def 76 ref appTerm appTerm 65 ref appTerm absTerm 405 def 76 ref appTerm 406 def betaConv nil 258 ref 405 ref appTerm 407 def axiom nil 42 ref 407 remove nil cons cons 43 ref 406 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 260 ref 261 ref 405 remove nil cons cons 264 ref cons nil cons cons 137 ref subst eqMp eqMp 408 def subst trans appThm nil 73 ref 65 ref nil cons cons nil cons nil cons cons 409 def 348 remove subst 410 def trans sym 79 ref eqMp eqMp eqMp nil 333 ref 86 ref 386 ref cons nil cons 411 def cons nil cons cons 99 ref subst deductAntisym eqMp nil 337 ref 387 remove cons nil cons cons 412 def 60 ref subst 412 remove 126 ref subst 393 remove "_536" 3 ref var 413 def 44 ref 12 ref 413 remove varTerm 414 def appTerm 47 ref appTerm appTerm 288 ref 250 ref 414 remove appTerm appTerm 47 ref appTerm appTerm absTerm 65 ref appTerm betaConv appThm 394 remove 44 ref 12 ref 65 ref appTerm 415 def 47 ref appTerm 416 def appTerm 288 ref 343 remove appTerm 417 def 47 ref appTerm appTerm refl appThm trans 398 remove 344 ref appThm eqMp sym 87 ref 83 remove 73 ref 44 ref 415 remove 76 ref appTerm appTerm 76 ref appTerm absTerm 418 def 76 ref appTerm 419 def betaConv nil 258 ref 418 ref appTerm 420 def axiom nil 42 ref 420 remove nil cons cons 43 ref 419 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 260 ref 261 ref 418 remove nil cons cons 264 ref cons nil cons cons 137 ref subst eqMp eqMp subst 421 def appThm 311 ref 350 ref appThm 422 def 55 remove appThm 330 remove trans appThm 332 remove trans sym 79 ref eqMp eqMp eqMp nil 355 ref 411 remove cons nil cons cons 99 ref subst deductAntisym eqMp 363 ref nil 355 ref 364 ref 365 ref 386 remove cons nil cons cons cons nil cons cons 381 ref subst proveHyp proveHyp proveHyp 423 def subst absThm appThm appThm nil "P" 230 ref var 424 def 245 ref nil cons cons nil cons nil cons cons "A" 229 ref nil cons 425 def cons nil cons 426 def 197 ref cons 427 def 87 ref 306 ref 383 ref nil "t" 114 ref var 118 ref nil cons 428 def cons nil cons nil cons cons "A" 113 ref nil cons 429 def cons 430 def "B" 4 ref cons nil cons cons 197 ref cons "t" 1 ref 113 ref 425 remove cons opType 431 def var 432 def 25 ref 1 ref 431 ref 1 ref 431 ref 4 ref cons opType 433 def nil cons cons opType constTerm 434 def 432 ref varTerm 435 def appTerm 121 ref 435 ref 122 ref appTerm absTerm 436 def appTerm 437 def absTerm 438 def 435 ref appTerm 439 def betaConv 0 ref 1 ref 433 ref 4 ref cons opType 440 def constTerm 441 def refl 432 ref 437 remove assume sym 434 remove 436 remove appTerm 435 ref appTerm 442 def assume sym deductAntisym absThm appThm nil 441 ref 432 remove 442 remove absTerm appTerm axiom eqMp nil 42 ref 441 ref 438 ref appTerm nil cons cons 43 ref 439 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp "A" 431 ref nil cons 443 def cons nil cons "P" 433 remove var 438 remove nil cons cons "x" 431 ref var 435 remove nil cons cons nil cons cons nil cons cons 137 ref subst eqMp eqMp subst subst 444 def appThm appThm appThm "Data.Bool.?" const 445 def 115 ref constTerm 446 def 121 ref 250 ref 123 ref appTerm 447 def absTerm 448 def appTerm refl appThm sym nil 128 ref 428 ref cons nil cons nil cons cons 449 def 128 ref 44 ref 250 ref 116 ref 121 ref 129 ref 122 ref appTerm 450 def absTerm 451 def appTerm appTerm appTerm 446 ref 121 ref 250 ref 450 ref appTerm absTerm 452 def appTerm appTerm absTerm 453 def 129 ref appTerm 454 def betaConv nil 0 ref 132 remove constTerm 455 def 453 ref appTerm 456 def axiom nil 42 ref 456 remove nil cons cons 43 ref 454 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp "A" 273 remove cons nil cons 457 def "P" 115 remove var 458 def 453 remove nil cons cons "x" 114 ref var 459 def 129 ref nil cons cons nil cons 460 def cons nil cons cons 137 ref subst eqMp eqMp subst eqMp 461 def subst 462 def subst 445 ref 231 remove constTerm 463 def refl 464 def 233 ref 306 ref 245 remove 238 ref appTerm betaConv appThm nil 117 ref 244 ref nil cons cons nil cons nil cons cons 461 ref subst 446 ref refl 465 def 121 ref 306 ref 244 remove 122 ref appTerm betaConv appThm nil 384 ref 43 ref 239 ref nil cons 466 def cons nil cons cons nil cons cons 467 def nil 286 remove 43 ref 44 ref 250 ref 48 ref appTerm appTerm 290 remove appTerm nil cons 468 def cons nil cons 469 def cons nil cons cons 470 def 60 ref subst 470 remove 126 ref subst 44 ref "_542" 3 ref var 471 def 44 ref 250 ref 12 ref 471 remove varTerm 472 def appTerm 47 ref appTerm appTerm appTerm 14 ref 472 remove appTerm 289 ref appTerm appTerm absTerm 473 def 45 ref appTerm 474 def appTerm refl 475 def 473 ref 254 ref appTerm betaConv appThm 87 ref 474 remove betaConv appThm 476 def 44 ref 250 ref 396 remove appTerm appTerm 302 remove appTerm refl appThm trans 473 remove refl 477 def 305 remove appThm eqMp sym 87 ref 306 ref 402 remove appThm 350 remove trans appThm 318 remove appThm nil 73 ref 281 ref cons nil cons nil cons cons 310 remove subst 319 ref trans trans sym 79 ref eqMp eqMp eqMp nil 333 remove 86 ref 468 ref cons nil cons 478 def cons nil cons cons 99 ref subst deductAntisym eqMp nil 337 remove 469 remove cons nil cons cons 479 def 60 ref subst 479 remove 126 ref subst 475 remove "_540" 3 ref var 480 def 44 ref 250 ref 12 ref 480 remove varTerm 481 def appTerm 47 ref appTerm appTerm appTerm 14 ref 481 remove appTerm 289 remove appTerm appTerm absTerm 65 ref appTerm betaConv appThm 476 remove 44 ref 250 ref 416 remove appTerm appTerm 342 remove appTerm refl appThm trans 477 remove 344 remove appThm eqMp sym 87 ref 306 ref 421 remove appThm appThm 349 remove appThm 354 remove trans sym 79 ref eqMp eqMp eqMp nil 355 ref 478 remove cons nil cons cons 99 ref subst deductAntisym eqMp 363 remove nil 355 remove 364 remove 365 ref 468 remove cons nil cons cons cons nil cons cons 381 ref subst proveHyp proveHyp proveHyp 482 def subst trans absThm appThm trans trans absThm appThm trans appThm appThm 19 ref nil 117 ref 242 ref nil cons cons nil cons nil cons cons 461 ref subst 465 ref 121 ref 306 ref 242 remove 122 ref appTerm betaConv appThm 385 remove 482 ref subst 19 ref 123 ref refl appThm 483 def nil 424 ref 240 ref nil cons 484 def cons nil cons nil cons cons 462 remove subst 464 ref 233 ref 306 ref 240 remove 238 ref appTerm betaConv 485 def appThm absThm appThm trans appThm trans trans absThm appThm trans appThm 232 ref refl 486 def 233 ref 383 ref 121 ref 467 remove 423 ref subst absThm appThm absThm appThm appThm appThm trans 311 ref 87 ref 14 ref 116 ref 121 ref 288 ref 447 ref appTerm 487 def 241 remove appTerm absTerm appTerm 488 def appTerm 489 def refl 490 def 464 ref 233 ref 233 ref 446 ref 121 ref 14 ref 123 ref appTerm 491 def 250 ref 239 ref appTerm 492 def appTerm 493 def absTerm 494 def appTerm absTerm 495 def 238 ref appTerm betaConv 496 def absThm appThm appThm appThm 464 ref 233 ref 490 ref 496 remove appThm absThm appThm appThm nil "q" 230 ref var 497 def 495 remove nil cons cons 42 ref 488 remove nil cons 498 def cons nil cons 499 def cons nil cons cons 427 ref "q" 114 remove var 500 def 44 ref 50 ref 446 ref 121 ref 500 ref varTerm 501 def 122 ref appTerm 502 def absTerm 503 def appTerm 504 def appTerm appTerm 446 ref 121 ref 50 remove 502 ref appTerm absTerm appTerm appTerm absTerm 505 def 501 ref appTerm 506 def betaConv 42 ref 455 ref 505 ref appTerm 507 def absTerm 508 def 45 ref appTerm 509 def betaConv nil 258 ref 508 ref appTerm 510 def axiom nil 42 ref 510 remove nil cons cons 43 ref 509 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 260 ref 261 ref 508 remove nil cons cons 271 ref cons nil cons cons 137 ref subst eqMp eqMp nil 42 ref 507 remove nil cons cons 43 ref 506 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 457 ref 458 ref 505 remove nil cons cons 459 ref 501 ref nil cons cons nil cons 511 def cons nil cons cons 137 ref subst eqMp eqMp 512 def subst 513 def subst eqMp 464 ref 233 ref 87 ref 490 ref 465 ref 121 ref 494 ref 122 ref appTerm betaConv 514 def absThm appThm appThm appThm 465 ref 121 ref 490 remove 514 remove appThm absThm appThm appThm nil 500 ref 494 remove nil cons cons 499 remove cons nil cons cons 512 remove subst eqMp absThm appThm trans appThm 19 ref 465 ref 121 ref 87 ref 483 ref 464 ref 233 ref 233 ref 492 ref absTerm 515 def 238 ref appTerm betaConv 516 def absThm appThm appThm appThm 464 ref 233 ref 483 remove 516 remove appThm absThm appThm appThm nil 497 ref 515 remove nil cons cons 384 ref nil cons cons nil cons cons 513 remove subst eqMp absThm appThm appThm 232 ref 233 ref 116 ref 121 ref 487 ref 239 remove appTerm 517 def absTerm appTerm absTerm 518 def appTerm 519 def refl 520 def appThm 87 ref 19 ref 465 ref 121 ref 121 ref 463 ref 233 ref 493 ref absTerm 521 def appTerm absTerm 522 def 122 ref appTerm betaConv 523 def absThm appThm appThm 520 ref appThm appThm 465 ref 121 ref 19 ref 523 remove appThm 520 ref appThm absThm appThm appThm nil 128 ref 522 remove nil cons cons 43 ref 519 ref nil cons 524 def cons nil cons 525 def cons nil cons cons 43 ref 44 ref 14 ref 446 ref 451 remove appTerm 526 def appTerm 47 ref appTerm appTerm 446 ref 121 ref 14 ref 450 ref appTerm 47 ref appTerm absTerm appTerm appTerm absTerm 527 def 47 ref appTerm 528 def betaConv 128 ref 258 ref 527 ref appTerm 529 def absTerm 530 def 129 ref appTerm 531 def betaConv nil 455 ref 530 ref appTerm 532 def axiom nil 42 ref 532 remove nil cons cons 43 ref 531 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 457 ref 458 ref 530 remove nil cons cons 460 ref cons nil cons cons 137 ref subst eqMp eqMp nil 42 ref 529 remove nil cons cons 43 ref 528 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 260 ref 261 ref 527 remove nil cons cons 331 ref cons nil cons cons 137 ref subst eqMp eqMp 533 def subst eqMp 465 ref 121 ref 87 ref 19 ref 464 ref 233 ref 521 ref 238 ref appTerm betaConv 534 def absThm appThm appThm 520 ref appThm appThm 464 ref 233 ref 19 ref 534 remove appThm 520 remove appThm absThm appThm appThm nil "p" 230 remove var 535 def 521 remove nil cons cons 525 remove cons nil cons cons 427 ref 533 ref subst subst eqMp absThm appThm trans trans appThm 87 ref 311 ref 464 ref 233 ref 233 ref 446 ref 121 ref 489 remove 493 ref appTerm 536 def absTerm 537 def appTerm absTerm 538 def 238 ref appTerm betaConv 539 def absThm appThm appThm 446 ref 121 ref 463 ref 233 ref 14 ref 493 ref appTerm 519 ref appTerm absTerm 540 def appTerm absTerm 541 def appTerm 542 def refl 543 def appThm appThm 464 ref 233 ref 311 ref 539 remove appThm 543 remove appThm absThm appThm appThm nil 535 remove 538 remove nil cons cons 43 ref 542 remove nil cons cons nil cons cons nil cons cons 427 ref 43 ref 44 ref 288 ref 526 ref appTerm 544 def 47 ref appTerm appTerm 446 ref 121 ref 288 ref 450 ref appTerm 545 def 47 ref appTerm absTerm appTerm appTerm absTerm 546 def 47 ref appTerm 547 def betaConv 128 ref 258 ref 546 ref appTerm 548 def absTerm 549 def 129 ref appTerm 550 def betaConv nil 455 ref 549 ref appTerm 551 def axiom nil 42 ref 551 remove nil cons cons 43 ref 550 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 457 ref 458 ref 549 remove nil cons cons 460 ref cons nil cons cons 137 ref subst eqMp eqMp nil 42 ref 548 remove nil cons cons 43 ref 547 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 260 ref 261 ref 546 remove nil cons cons 331 remove cons nil cons cons 137 ref subst eqMp eqMp subst subst eqMp 464 ref 233 ref 87 ref 311 ref 465 ref 121 ref 537 ref 122 ref appTerm betaConv 552 def absThm appThm appThm 465 ref 121 ref 541 ref 122 ref appTerm betaConv 553 def absThm appThm appThm appThm 465 ref 121 ref 311 ref 552 remove appThm 553 remove appThm absThm appThm appThm nil 128 ref 537 remove nil cons cons 500 ref 541 remove nil cons cons nil cons cons nil cons cons 500 ref 44 ref 544 remove 504 ref appTerm appTerm 446 ref 121 ref 545 remove 502 ref appTerm absTerm appTerm appTerm absTerm 554 def 501 ref appTerm 555 def betaConv 128 ref 455 ref 554 ref appTerm 556 def absTerm 557 def 129 ref appTerm 558 def betaConv nil 455 ref 557 ref appTerm 559 def axiom nil 42 ref 559 remove nil cons cons 43 ref 558 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 457 ref 458 ref 557 remove nil cons cons 460 ref cons nil cons cons 137 ref subst eqMp eqMp nil 42 ref 556 remove nil cons cons 43 ref 555 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 457 ref 458 ref 554 remove nil cons cons 511 ref cons nil cons cons 137 ref subst eqMp eqMp subst eqMp 465 ref 121 ref 87 ref 288 ref 536 ref appTerm 560 def refl 561 def 464 ref 233 ref 540 ref 238 ref appTerm betaConv absThm appThm appThm appThm 464 remove "y'" 229 ref var 562 def 561 remove 540 ref 562 ref varTerm 563 def appTerm betaConv appThm absThm appThm appThm nil 497 ref 540 remove nil cons cons 42 ref 536 remove nil cons 564 def cons 565 def nil cons cons nil cons cons 427 ref 500 ref 44 ref 288 ref 45 ref appTerm 566 def 504 remove appTerm appTerm 446 ref 121 ref 566 ref 502 remove appTerm absTerm 567 def appTerm appTerm absTerm 568 def 501 ref appTerm 569 def betaConv 42 ref 455 ref 568 ref appTerm 570 def absTerm 571 def 45 ref appTerm 572 def betaConv nil 258 ref 571 ref appTerm 573 def axiom nil 42 ref 573 remove nil cons cons 43 ref 572 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 260 ref 261 ref 571 remove nil cons cons 271 ref cons nil cons cons 137 ref subst eqMp eqMp nil 42 ref 570 remove nil cons cons 43 ref 569 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 457 ref 458 ref 568 remove nil cons cons 511 ref cons nil cons cons 137 ref subst eqMp eqMp 574 def subst subst eqMp absThm appThm trans absThm appThm trans trans trans 279 remove assume eqMp nil 42 ref 463 ref 233 ref 446 ref 121 ref 463 remove 562 ref 560 remove 14 ref 491 remove 250 ref 237 ref 563 ref appTerm 575 def appTerm 576 def appTerm 577 def appTerm 519 remove appTerm 578 def appTerm 579 def absTerm 580 def appTerm 581 def absTerm 582 def appTerm 583 def absTerm 584 def appTerm 585 def nil cons cons 282 ref cons nil cons cons 106 ref subst proveHyp nil 424 ref 233 ref 12 ref 584 ref 238 ref appTerm 586 def appTerm 254 ref appTerm 587 def absTerm nil cons cons nil cons nil cons cons 427 ref 198 ref subst 588 def subst 233 ref nil 73 ref 587 remove nil cons cons nil cons nil cons cons 80 ref subst nil 42 ref 586 ref nil cons 589 def cons 282 ref cons nil cons cons 590 def 60 ref subst 590 remove 126 ref subst 586 ref betaConv 586 remove assume eqMp nil 42 ref 583 ref nil cons cons 282 ref cons nil cons cons 106 ref subst proveHyp nil 117 ref 121 ref 12 ref 582 ref 122 ref appTerm 591 def appTerm 254 ref appTerm 592 def absTerm 593 def nil cons cons nil cons nil cons cons 198 ref subst 121 ref nil 73 ref 592 remove nil cons cons nil cons nil cons cons 80 ref subst nil 42 ref 591 ref nil cons 594 def cons 282 ref cons nil cons cons 595 def 60 ref subst 595 remove 126 ref subst 591 ref betaConv 591 remove assume eqMp nil 42 ref 581 ref nil cons cons 282 ref cons nil cons cons 106 ref subst proveHyp nil 424 ref 562 ref 12 ref 580 ref 563 ref appTerm 596 def appTerm 254 ref appTerm 597 def absTerm nil cons cons nil cons nil cons cons 588 remove subst 562 remove nil 73 ref 597 remove nil cons cons nil cons nil cons cons 80 ref subst nil 42 ref 596 ref nil cons 598 def cons 282 ref cons nil cons cons 599 def 60 ref subst 599 remove 126 ref subst 596 ref betaConv 596 remove assume eqMp nil 42 ref 579 remove nil cons 600 def cons 282 ref cons nil cons cons 601 def 106 ref subst proveHyp 601 ref 60 ref subst 601 remove 126 ref subst nil 42 ref 578 remove nil cons 602 def cons 282 ref cons nil cons cons 603 def 60 ref subst 603 remove 126 ref subst nil "_14620" 229 ref var 604 def 563 remove nil cons cons nil cons nil cons cons nil 85 ref 577 remove nil cons cons 86 ref 524 ref cons nil cons cons nil cons cons 605 def 99 ref subst 606 def nil 85 ref 124 remove cons 607 def 86 ref 576 remove nil cons cons nil cons cons nil cons cons 608 def 99 ref subst proveHyp nil 384 ref 43 ref 237 ref 604 remove varTerm 609 def appTerm 610 def nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp nil "_14621" 113 ref var 611 def 122 ref nil cons 612 def cons nil cons nil cons cons nil "b" 3 ref var 613 def 250 ref 118 ref 611 remove varTerm 614 def appTerm 615 def appTerm nil cons 616 def cons "a" 3 ref var 617 def 236 ref 614 ref appTerm 609 ref appTerm 618 def nil cons 619 def cons nil cons cons nil cons cons nil 42 ref 44 ref 617 ref varTerm 620 def appTerm 621 def 254 ref appTerm 622 def nil cons 623 def cons 624 def 43 ref 44 ref 288 ref 620 ref appTerm 613 ref varTerm 625 def appTerm appTerm 12 ref 250 ref 625 ref appTerm 626 def appTerm 627 def 620 ref appTerm appTerm nil cons 628 def cons nil cons 629 def cons nil cons cons 630 def 60 ref subst 630 remove 126 ref subst 44 ref "_606" 3 ref var 631 def 44 ref 288 ref 631 remove varTerm 632 def appTerm 625 ref appTerm appTerm 627 ref 632 remove appTerm appTerm absTerm 633 def 620 ref appTerm 634 def appTerm refl 635 def 633 ref 254 ref appTerm betaConv appThm 87 ref 634 remove betaConv appThm 636 def 44 ref 325 remove 625 ref appTerm appTerm 627 ref 254 ref appTerm appTerm refl appThm trans 633 remove refl 637 def 622 remove assume 638 def appThm eqMp sym 87 ref nil 73 ref 625 ref nil cons 639 def cons nil cons nil cons cons 640 def 329 ref subst appThm nil 73 ref 626 ref nil cons 641 def cons nil cons nil cons cons 642 def 265 ref subst 640 ref 269 ref subst trans appThm nil 262 ref 639 remove cons nil cons nil cons cons 277 ref subst trans sym 79 ref eqMp eqMp eqMp nil 85 ref 623 ref cons 643 def 86 ref 628 ref cons nil cons 644 def cons nil cons cons 99 ref subst deductAntisym eqMp nil 42 ref 621 remove 65 ref appTerm 645 def nil cons 646 def cons 647 def 629 remove cons nil cons cons 648 def 60 ref subst 648 remove 126 ref subst 635 remove "_604" 3 ref var 649 def 44 ref 288 ref 649 remove varTerm 650 def appTerm 625 ref appTerm appTerm 627 ref 650 remove appTerm appTerm absTerm 65 ref appTerm betaConv appThm 636 remove 44 ref 404 remove 625 ref appTerm appTerm 627 remove 65 ref appTerm appTerm refl appThm trans 637 remove 645 remove assume 651 def appThm eqMp sym 87 ref 640 ref 408 ref subst appThm 642 ref 73 ref 44 ref 253 remove 65 ref appTerm appTerm 65 ref appTerm absTerm 652 def 76 ref appTerm 653 def betaConv nil 258 ref 652 ref appTerm 654 def axiom nil 42 ref 654 remove nil cons cons 43 ref 653 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 260 ref 261 ref 652 remove nil cons cons 264 ref cons nil cons cons 137 ref subst eqMp eqMp 655 def subst appThm 410 ref trans sym 79 ref eqMp eqMp eqMp nil 85 ref 646 remove cons 656 def 644 remove cons nil cons cons 99 ref subst deductAntisym eqMp 357 ref 620 ref appTerm 657 def betaConv 360 ref nil 361 ref 43 ref 657 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 260 ref 362 ref 262 ref 620 ref nil cons 658 def cons nil cons cons nil cons cons 137 ref subst eqMp eqMp 659 def nil 656 ref 86 ref 623 remove cons 660 def 365 ref 628 remove cons nil cons cons cons nil cons cons 381 ref subst proveHyp proveHyp proveHyp 661 def subst 13 ref nil 617 ref 615 remove nil cons cons nil cons nil cons cons nil 73 ref 658 remove cons nil cons nil cons cons 269 remove subst 662 def subst appThm 618 remove refl appThm trans nil 43 ref 619 remove cons 42 ref 616 remove cons nil cons cons nil cons cons nil "t2" 3 ref var 663 def 82 remove cons "t1" 3 ref var 664 def 74 remove cons nil cons cons nil cons cons 663 ref 44 ref 288 ref 664 ref varTerm 665 def appTerm 663 remove varTerm 666 def appTerm appTerm 288 ref 666 ref appTerm 665 ref appTerm appTerm absTerm 667 def 666 ref appTerm 668 def betaConv 664 remove 258 ref 667 ref appTerm 669 def absTerm 670 def 665 ref appTerm 671 def betaConv nil 258 ref 670 ref appTerm 672 def axiom nil 42 ref 672 remove nil cons cons 43 ref 671 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 260 ref 261 ref 670 remove nil cons cons 262 ref 665 remove nil cons cons nil cons cons nil cons cons 137 ref subst eqMp eqMp nil 42 ref 669 remove nil cons cons 43 ref 668 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 260 ref 261 ref 667 remove nil cons cons 262 ref 666 remove nil cons cons nil cons cons nil cons cons 137 ref subst eqMp eqMp subst 673 def subst 121 ref 487 remove 610 remove appTerm absTerm 674 def 614 ref appTerm 675 def betaConv 518 ref 609 ref appTerm 676 def betaConv 605 remove 203 ref subst nil 42 ref 524 remove cons 43 ref 676 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 426 ref 424 ref 518 remove nil cons cons "x" 229 ref var 677 def 609 remove nil cons cons nil cons cons nil cons cons 137 ref subst eqMp eqMp nil 42 ref 116 ref 674 ref appTerm nil cons cons 43 ref 675 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 430 ref nil cons 678 def 117 ref 674 remove nil cons cons 121 ref 614 remove nil cons cons nil cons cons nil cons cons 137 ref subst eqMp eqMp eqMp eqMp subst eqMp subst nil 42 ref 575 remove nil cons cons 679 def 282 ref cons nil cons cons 106 ref subst proveHyp nil 679 remove nil cons nil cons cons 44 ref 251 remove appTerm refl 75 remove 265 ref subst appThm nil 262 ref 252 remove cons nil cons nil cons cons 277 ref subst trans sym 79 ref eqMp 680 def subst 606 remove 608 remove 203 ref subst proveHyp eqMp eqMp eqMp nil 85 ref 602 ref cons 86 ref 281 ref cons nil cons 681 def cons nil cons cons 99 ref subst deductAntisym eqMp nil 565 remove 282 ref cons nil cons cons 682 def 60 ref subst 682 remove 126 ref subst nil "_14619" 229 ref var 683 def 238 ref nil cons cons nil cons nil cons cons nil 85 ref 498 remove cons 86 ref 493 remove nil cons cons nil cons cons nil cons cons 684 def 203 ref subst 685 def nil 607 remove 86 ref 492 remove nil cons cons nil cons cons nil cons cons 686 def 99 ref subst proveHyp nil 384 ref 43 ref 237 remove 683 remove varTerm 687 def appTerm nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp nil "_14618" 113 ref var 688 def 612 ref cons nil cons nil cons cons nil 613 ref 250 ref 118 ref 688 remove varTerm 689 def appTerm 690 def appTerm 691 def nil cons 692 def cons 617 ref 236 remove 689 ref appTerm 693 def 687 ref appTerm 694 def nil cons 695 def cons nil cons cons nil cons cons 661 remove subst 13 ref nil 617 ref 690 remove nil cons cons nil cons nil cons cons 662 remove subst appThm 694 remove refl appThm trans nil 43 ref 695 remove cons 42 ref 692 remove cons nil cons cons nil cons cons 673 remove subst 233 ref 288 ref 691 remove appTerm 693 remove 238 ref appTerm appTerm absTerm 696 def 687 ref appTerm 697 def betaConv 121 ref 232 ref 233 ref 517 remove absTerm appTerm absTerm 698 def 689 ref appTerm 699 def betaConv 383 ref 121 ref 87 ref 311 ref 447 ref refl appThm 700 def 486 ref 233 ref 485 ref absThm appThm appThm appThm 486 remove 233 ref 700 remove 485 remove appThm absThm appThm appThm nil 497 remove 484 remove cons 42 ref 447 remove nil cons cons nil cons cons nil cons cons 427 remove 500 ref 44 ref 566 remove 116 ref 503 remove appTerm appTerm appTerm 116 ref 567 remove appTerm appTerm absTerm 701 def 501 remove appTerm 702 def betaConv 42 ref 455 ref 701 ref appTerm 703 def absTerm 704 def 45 remove appTerm 705 def betaConv nil 258 ref 704 ref appTerm 706 def axiom nil 42 ref 706 remove nil cons cons 43 ref 705 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 260 ref 261 ref 704 remove nil cons cons 271 remove cons nil cons cons 137 ref subst eqMp eqMp nil 42 ref 703 remove nil cons cons 43 ref 702 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 457 ref 458 ref 701 remove nil cons cons 511 remove cons nil cons cons 137 ref subst eqMp eqMp subst subst eqMp absThm appThm 684 remove 99 ref subst eqMp nil 42 ref 116 ref 698 ref appTerm nil cons cons 43 ref 699 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 678 ref 117 ref 698 remove nil cons cons 121 ref 689 remove nil cons cons nil cons cons nil cons cons 137 ref subst eqMp eqMp nil 42 ref 232 ref 696 ref appTerm nil cons cons 43 ref 697 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 426 ref 424 ref 696 remove nil cons cons 677 ref 687 remove nil cons cons nil cons cons nil cons cons 137 ref subst eqMp eqMp eqMp eqMp subst eqMp subst nil 42 ref 466 remove cons 707 def 282 ref cons nil cons cons 106 ref subst proveHyp nil 707 remove nil cons nil cons cons 680 ref subst 685 remove 686 remove 203 ref subst proveHyp eqMp eqMp eqMp nil 85 ref 564 remove cons 708 def 681 ref cons nil cons cons 99 ref subst deductAntisym eqMp nil 708 remove 86 ref 602 remove cons 365 ref 281 remove cons nil cons 709 def cons cons nil cons cons 381 ref subst proveHyp proveHyp eqMp nil 85 ref 600 remove cons 681 ref cons nil cons cons 99 ref subst deductAntisym eqMp eqMp eqMp nil 85 ref 598 remove cons 681 ref cons nil cons cons 99 ref subst deductAntisym eqMp eqMp absThm eqMp nil 42 ref 232 ref 677 ref 12 ref 580 ref 677 ref varTerm 710 def appTerm appTerm 254 ref appTerm absTerm appTerm nil cons cons 43 ref 12 ref 581 remove appTerm 254 ref appTerm nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 426 ref 424 ref 580 remove nil cons cons 681 ref cons nil cons cons nil 42 ref 116 ref 121 ref 228 ref 90 ref appTerm absTerm 711 def appTerm 712 def nil cons 713 def cons 714 def 43 ref 12 ref 446 ref 118 ref appTerm 715 def appTerm 716 def 90 ref appTerm nil cons 717 def cons nil cons cons nil cons cons 718 def 60 ref subst 718 remove 126 ref subst nil 42 ref 715 ref nil cons 719 def cons 720 def 43 ref 90 ref nil cons 721 def cons nil cons 722 def cons nil cons cons 723 def 60 ref subst 723 remove 126 ref subst nil 714 ref 722 ref cons nil cons cons 724 def 106 ref subst 43 ref 12 ref 116 ref 121 ref 228 remove 47 ref appTerm absTerm appTerm appTerm 47 ref appTerm absTerm 725 def 90 ref appTerm 726 def betaConv nil 720 remove 43 ref 258 ref 725 ref appTerm 727 def nil cons 728 def cons nil cons cons nil cons cons 729 def 106 ref subst 44 ref 715 remove appTerm 730 def refl 128 ref 258 ref 43 ref 12 ref 116 ref 121 ref 12 ref 450 remove appTerm 47 ref appTerm absTerm appTerm appTerm 47 remove appTerm absTerm appTerm absTerm 731 def 118 ref appTerm betaConv appThm nil 133 remove 446 ref appTerm 731 remove appTerm axiom 134 remove appThm eqMp 732 def nil 42 ref 730 remove 727 ref appTerm nil cons cons 43 ref 716 remove 727 remove appTerm nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 729 remove nil 42 ref 287 ref nil cons 733 def cons 43 ref 48 remove nil cons 734 def cons nil cons cons nil cons cons 735 def 60 ref subst 735 remove 126 ref subst 60 ref 126 ref 287 remove assume 81 remove eqMp eqMp 100 remove deductAntisym eqMp eqMp nil 85 ref 733 remove cons 86 ref 734 remove cons nil cons cons nil cons cons 99 ref subst deductAntisym eqMp subst eqMp eqMp nil 42 ref 728 remove cons 43 ref 726 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 260 ref 261 ref 725 remove nil cons cons 262 ref 721 ref cons nil cons 736 def cons nil cons cons 137 ref subst eqMp eqMp eqMp eqMp nil 85 ref 719 remove cons 86 ref 721 ref cons nil cons 737 def cons nil cons cons 99 ref subst deductAntisym eqMp eqMp nil 85 ref 713 remove cons 738 def 86 ref 717 remove cons nil cons cons nil cons cons 99 ref subst deductAntisym eqMp 739 def subst eqMp eqMp eqMp nil 85 ref 594 remove cons 681 ref cons nil cons cons 99 ref subst deductAntisym eqMp eqMp absThm eqMp nil 42 ref 116 ref 593 remove appTerm nil cons cons 43 ref 12 ref 583 remove appTerm 254 ref appTerm nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 678 ref 117 ref 582 remove nil cons cons 681 ref cons nil cons cons 739 ref subst eqMp eqMp eqMp nil 85 ref 589 remove cons 681 ref cons nil cons cons 99 ref subst deductAntisym eqMp eqMp absThm eqMp nil 42 ref 232 ref 677 remove 12 ref 584 ref 710 remove appTerm appTerm 254 ref appTerm absTerm appTerm nil cons cons 43 ref 12 ref 585 remove appTerm 254 ref appTerm nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 426 remove 424 remove 584 remove nil cons cons 681 ref cons nil cons cons 739 ref subst eqMp eqMp eqMp nil 85 ref 280 remove cons 681 ref cons nil cons cons 99 ref subst deductAntisym eqMp eqMp subst 740 def subst eqMp 144 ref 224 ref 87 ref 144 ref 152 ref 220 remove 12 ref 213 ref 225 ref appTerm appTerm 15 ref 225 ref appTerm 741 def appTerm refl appThm absThm appThm appThm 13 ref 219 remove 225 ref appTerm betaConv appThm 741 ref refl appThm appThm nil 226 remove 86 ref 741 ref nil cons cons "e" 2 ref var 742 def 225 ref nil cons 743 def cons nil cons cons cons nil cons cons 206 ref nil 42 ref 44 ref 116 ref "m" 113 ref var 744 def 12 ref 118 ref 744 ref varTerm 745 def appTerm 746 def appTerm 747 def 12 ref 275 ref 745 ref appTerm "e" 113 ref var 748 def varTerm 749 def appTerm 750 def appTerm 90 ref appTerm appTerm absTerm appTerm appTerm 12 ref 118 ref 749 ref appTerm 751 def appTerm 90 ref appTerm appTerm 752 def nil cons cons nil cons nil cons cons 278 ref subst sym 753 def 117 ref 12 ref 250 ref 752 ref appTerm appTerm 254 ref appTerm absTerm 754 def 118 ref appTerm 755 def betaConv 748 ref 455 ref 754 ref appTerm 756 def absTerm 757 def 749 ref appTerm 758 def betaConv 86 ref 116 ref 757 ref appTerm 759 def absTerm 760 def 90 ref appTerm 761 def betaConv 258 ref refl 762 def 86 ref 383 ref 748 ref 455 ref refl 763 def 117 ref 753 remove absThm appThm absThm appThm absThm appThm 87 ref 762 remove 86 ref 86 ref 116 ref 748 ref 455 ref 117 ref 752 remove absTerm appTerm absTerm appTerm absTerm 764 def 90 ref appTerm betaConv absThm appThm appThm 19 ref 764 ref 65 ref appTerm betaConv appThm 764 ref 254 ref appTerm betaConv appThm appThm nil "p" 9 ref var 765 def 764 remove nil cons cons nil cons nil cons cons 765 ref 44 ref 258 ref 613 ref 765 remove varTerm 766 def 625 ref appTerm absTerm appTerm appTerm 14 ref 766 ref 65 ref appTerm appTerm 766 ref 254 ref appTerm appTerm appTerm absTerm 767 def 766 ref appTerm 768 def betaConv nil 0 ref 1 ref 68 ref 4 ref cons opType constTerm 767 ref appTerm 769 def axiom nil 42 ref 769 remove nil cons cons 43 ref 768 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp "A" 10 remove cons nil cons "P" 68 remove var 767 remove nil cons cons "x" 9 remove var 766 remove nil cons cons nil cons cons nil cons cons 137 ref subst eqMp eqMp subst eqMp 19 ref 383 ref 748 ref 763 ref 117 ref 87 ref 383 ref 744 ref 747 ref refl 770 def nil 73 ref 750 ref nil cons 771 def cons nil cons nil cons cons 772 def 655 ref subst appThm nil 73 ref 746 ref nil cons 773 def cons nil cons nil cons cons 655 ref subst trans absThm appThm 409 ref 73 ref 44 ref 116 ref 121 ref 76 ref absTerm appTerm appTerm 76 ref appTerm absTerm 774 def 76 ref appTerm 775 def betaConv nil 258 ref 774 ref appTerm 776 def axiom nil 42 ref 776 remove nil cons cons 43 ref 775 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 260 ref 261 ref 774 remove nil cons cons 264 ref cons nil cons cons 137 ref subst eqMp eqMp 777 def subst 778 def trans appThm nil 73 ref 751 ref nil cons 779 def cons nil cons nil cons cons 780 def 655 remove subst appThm 410 ref trans absThm appThm 409 ref 457 ref 197 ref cons 781 def 777 ref subst subst trans absThm appThm 778 remove trans appThm 383 ref 748 ref 763 remove 117 ref 87 ref 383 ref 744 ref 770 remove 772 remove 265 ref subst appThm absThm appThm appThm 780 remove 265 remove subst appThm absThm appThm absThm appThm appThm nil 73 ref 116 ref 748 ref 455 ref 117 ref 44 ref 116 ref 744 ref 747 remove 250 ref 750 ref appTerm 782 def appTerm absTerm 783 def appTerm 784 def appTerm 250 ref 751 ref appTerm 785 def appTerm 786 def absTerm 787 def appTerm 788 def absTerm 789 def appTerm nil cons cons nil cons nil cons cons 324 ref subst trans trans trans sym nil 117 ref 789 remove nil cons cons nil cons nil cons cons 198 ref subst 748 remove nil 73 ref 788 remove nil cons cons nil cons nil cons cons 80 ref subst nil 458 ref 787 remove nil cons cons nil cons nil cons cons 781 remove 198 ref subst subst 117 ref nil 73 ref 786 ref nil cons 790 def cons nil cons nil cons cons 80 ref subst nil 42 ref 790 remove cons nil cons nil cons cons 278 ref subst sym nil 42 ref 250 ref 786 remove appTerm 791 def nil cons 792 def cons 282 ref cons nil cons cons 793 def 60 ref subst 793 remove 126 ref subst nil 42 ref 784 remove nil cons cons 43 ref 785 ref nil cons 794 def cons nil cons 795 def cons nil cons cons 382 remove subst 311 remove 19 ref 383 remove 744 ref nil 42 ref 773 ref cons 43 ref 782 ref nil cons cons nil cons cons nil cons cons 796 def 423 remove subst absThm appThm appThm nil 42 ref 779 ref cons 797 def nil cons nil cons cons 798 def 270 ref subst appThm appThm 19 ref nil 117 ref 783 ref nil cons cons nil cons nil cons cons 461 remove subst 465 ref 744 ref 306 ref 783 remove 745 ref appTerm betaConv appThm 796 remove 482 ref subst 19 ref 746 ref refl appThm nil 42 ref 771 ref cons nil cons nil cons cons 270 remove subst appThm trans trans absThm appThm trans appThm 785 ref refl 799 def appThm appThm trans 288 ref 14 ref 116 ref 744 ref 288 ref 250 ref 746 ref appTerm appTerm 782 remove appTerm absTerm 800 def appTerm 801 def appTerm 751 ref appTerm 802 def appTerm 803 def refl 804 def 87 ref 19 ref 465 ref 744 ref 744 ref 14 ref 746 remove appTerm 750 remove appTerm 805 def absTerm 806 def 745 ref appTerm betaConv 807 def absThm appThm appThm 799 ref appThm appThm 465 ref 744 ref 19 ref 807 remove appThm 799 remove appThm absThm appThm appThm nil 128 ref 806 remove nil cons cons 795 remove cons nil cons cons 533 remove subst eqMp appThm 87 ref 804 ref 465 ref 744 ref 744 ref 14 ref 805 ref appTerm 785 remove appTerm 808 def absTerm 809 def 745 ref appTerm betaConv 810 def absThm appThm appThm appThm 465 ref 744 ref 804 remove 810 remove appThm absThm appThm appThm nil 500 remove 809 remove nil cons cons 42 ref 802 remove nil cons 811 def cons 812 def nil cons cons nil cons cons 574 remove subst eqMp trans trans 791 remove assume eqMp nil 42 ref 446 remove 744 ref 803 remove 808 ref appTerm 813 def absTerm 814 def appTerm 815 def nil cons cons 282 ref cons nil cons cons 106 ref subst proveHyp nil 117 ref 744 ref 12 ref 814 ref 745 ref appTerm 816 def appTerm 254 ref appTerm 817 def absTerm nil cons cons nil cons nil cons cons 198 ref subst 744 remove nil 73 ref 817 remove nil cons cons nil cons nil cons cons 80 ref subst nil 42 ref 816 ref nil cons 818 def cons 282 ref cons nil cons cons 819 def 60 ref subst 819 remove 126 ref subst 816 ref betaConv 816 remove assume eqMp nil 42 ref 813 remove nil cons 820 def cons 282 ref cons nil cons cons 821 def 106 ref subst proveHyp 821 ref 60 ref subst 821 remove 126 ref subst nil 42 ref 808 remove nil cons 822 def cons 282 ref cons nil cons cons 823 def 60 ref subst 823 remove 126 ref subst 44 ref "_14627" 113 ref var 824 def 118 ref 824 remove varTerm appTerm absTerm 825 def 745 remove appTerm 826 def appTerm refl 825 remove 749 ref appTerm betaConv appThm 87 ref 826 remove betaConv appThm 751 ref refl appThm trans 121 ref 123 remove absTerm refl nil 85 ref 805 remove nil cons cons 86 ref 794 remove cons nil cons cons nil cons cons 827 def 99 ref subst 828 def nil 85 ref 773 remove cons 86 ref 771 remove cons nil cons cons nil cons cons 829 def 203 ref subst proveHyp appThm eqMp 828 remove 829 remove 99 ref subst proveHyp eqMp nil 797 ref 282 ref cons nil cons cons 106 ref subst proveHyp 798 remove 680 ref subst 827 remove 203 ref subst eqMp eqMp eqMp nil 85 ref 822 ref cons 681 ref cons nil cons cons 99 ref subst deductAntisym eqMp nil 812 remove 282 ref cons nil cons cons 830 def 60 ref subst 830 remove 126 ref subst nil 85 ref 801 remove nil cons 831 def cons 86 ref 779 remove cons nil cons cons nil cons cons 832 def 203 ref subst nil 797 remove 43 ref 275 ref 749 ref appTerm 749 ref appTerm 833 def nil cons cons nil cons cons nil cons cons 126 ref subst proveHyp nil 121 ref 749 ref nil cons 834 def cons nil cons 835 def nil cons cons 136 remove subst eqMp nil 42 ref 14 ref 751 remove appTerm 833 remove appTerm nil cons cons 282 ref cons nil cons cons 106 ref subst proveHyp nil "_14622" 113 ref var 836 def 834 remove cons nil cons nil cons cons nil 613 remove 275 ref 836 remove varTerm 837 def appTerm 749 remove appTerm 838 def nil cons cons 617 remove 118 remove 837 ref appTerm 839 def nil cons cons nil cons cons nil cons cons nil 624 remove 43 ref 44 ref 288 ref 250 ref 620 ref appTerm appTerm 626 ref appTerm appTerm 250 ref 14 ref 620 ref appTerm 625 ref appTerm appTerm appTerm nil cons 840 def cons nil cons 841 def cons nil cons cons 842 def 60 ref subst 842 remove 126 ref subst 44 ref "_614" 3 ref var 843 def 44 ref 288 ref 250 ref 843 remove varTerm 844 def appTerm appTerm 626 ref appTerm appTerm 250 ref 14 ref 844 remove appTerm 625 ref appTerm appTerm appTerm absTerm 845 def 620 remove appTerm 846 def appTerm refl 847 def 845 ref 254 ref appTerm betaConv appThm 87 ref 846 remove betaConv appThm 848 def 44 ref 397 remove 626 ref appTerm appTerm 250 ref 301 remove 625 ref appTerm appTerm appTerm refl appThm trans 845 remove refl 849 def 638 remove appThm eqMp sym 87 ref 403 remove 626 ref refl 850 def appThm 642 ref 408 remove subst trans appThm 306 ref 640 ref 317 remove subst appThm 319 remove trans appThm 410 remove trans sym 79 ref eqMp eqMp eqMp nil 643 remove 86 ref 840 ref cons nil cons 851 def cons nil cons cons 99 ref subst deductAntisym eqMp nil 647 remove 841 remove cons nil cons cons 852 def 60 ref subst 852 remove 126 ref subst 847 remove "_612" 3 ref var 853 def 44 ref 288 ref 250 ref 853 remove varTerm 854 def appTerm appTerm 626 ref appTerm appTerm 250 ref 14 ref 854 remove appTerm 625 ref appTerm appTerm appTerm absTerm 65 ref appTerm betaConv appThm 848 remove 44 ref 417 remove 626 remove appTerm appTerm 250 ref 320 remove 625 remove appTerm appTerm appTerm refl appThm trans 849 remove 651 remove appThm eqMp sym 87 ref 422 remove 850 remove appThm 642 remove 329 remove subst trans appThm 306 ref 640 remove 324 ref subst appThm appThm nil 262 ref 641 remove cons nil cons nil cons cons 277 remove subst trans sym 79 ref eqMp eqMp eqMp nil 656 ref 851 remove cons nil cons cons 99 ref subst deductAntisym eqMp 659 remove nil 656 remove 660 remove 365 ref 840 remove cons nil cons cons cons nil cons cons 381 ref subst proveHyp proveHyp proveHyp subst nil 42 ref 14 ref 839 remove appTerm 838 remove appTerm nil cons cons nil cons nil cons cons 680 ref subst trans 800 ref 837 ref appTerm 855 def betaConv 832 remove 99 ref subst nil 42 ref 831 remove cons 43 ref 855 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 678 ref 117 ref 800 remove nil cons cons 121 ref 837 remove nil cons cons nil cons cons nil cons cons 137 ref subst eqMp eqMp eqMp subst eqMp eqMp nil 85 ref 811 remove cons 856 def 681 ref cons nil cons cons 99 ref subst deductAntisym eqMp nil 856 remove 86 ref 822 remove cons 709 remove cons cons nil cons cons 381 ref subst proveHyp proveHyp eqMp nil 85 ref 820 remove cons 681 ref cons nil cons cons 99 ref subst deductAntisym eqMp eqMp eqMp nil 85 ref 818 remove cons 681 ref cons nil cons cons 99 ref subst deductAntisym eqMp eqMp absThm eqMp nil 42 ref 116 ref 121 ref 12 ref 814 ref 122 ref appTerm appTerm 254 ref appTerm absTerm appTerm nil cons cons 43 ref 12 ref 815 remove appTerm 254 ref appTerm nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 678 ref 117 ref 814 remove nil cons cons 681 ref cons nil cons cons 739 ref subst eqMp eqMp eqMp nil 85 ref 792 remove cons 681 ref cons nil cons cons 99 ref subst deductAntisym eqMp eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp nil 42 ref 258 ref 760 ref appTerm nil cons cons 43 ref 761 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 260 ref 261 ref 760 remove nil cons cons 736 remove cons nil cons cons 137 ref subst eqMp eqMp nil 42 ref 759 remove nil cons cons 43 ref 758 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 678 ref 117 ref 757 remove nil cons cons 835 remove cons nil cons cons 137 ref subst eqMp eqMp nil 42 ref 756 remove nil cons cons 43 ref 755 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 457 ref 458 ref 754 remove nil cons cons 459 remove 428 remove cons nil cons cons nil cons cons 137 ref subst eqMp eqMp eqMp subst 857 def subst eqMp absThm appThm trans appThm 145 ref refl 858 def appThm sym nil 42 ref 40 ref 224 ref 12 ref 209 ref 225 ref appTerm 859 def 32 ref appTerm appTerm 741 ref appTerm absTerm appTerm 860 def nil cons 861 def cons 43 ref 208 ref cons nil cons 862 def cons nil cons cons 863 def 60 ref subst 863 remove 126 ref subst 152 ref 288 ref 213 ref 16 ref appTerm appTerm 445 ref 6 remove constTerm 864 def 21 ref 213 remove 157 ref appTerm absTerm appTerm appTerm absTerm 865 def 32 ref appTerm 866 def betaConv nil 40 ref 865 ref appTerm 867 def axiom 868 def nil 42 ref 867 remove nil cons cons 869 def 43 ref 866 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 865 ref nil cons cons 870 def 112 ref cons nil cons cons 137 ref subst eqMp eqMp nil 42 ref 288 ref 28 ref 32 ref appTerm 871 def 16 ref appTerm 872 def appTerm 864 ref 224 ref 871 ref 34 ref 225 ref appTerm 873 def appTerm 874 def absTerm 875 def appTerm 876 def appTerm nil cons 877 def cons 862 ref cons nil cons cons 878 def 106 ref subst proveHyp 878 ref 60 ref subst 878 remove 126 ref subst nil 109 ref 224 ref 12 ref 875 ref 225 ref appTerm 879 def appTerm 145 ref appTerm 880 def absTerm nil cons cons nil cons nil cons cons 207 ref subst 224 ref nil 73 ref 880 remove nil cons cons nil cons nil cons cons 80 ref subst nil 42 ref 879 ref nil cons 881 def cons 862 ref cons nil cons cons 882 def 60 ref subst 882 remove 126 ref subst 879 ref betaConv 879 remove assume eqMp nil 42 ref 874 ref nil cons 883 def cons 862 ref cons nil cons cons 884 def 106 ref subst proveHyp 884 ref 60 ref subst 884 remove 126 ref subst 44 ref "_30342" 2 ref var 885 def 15 ref 885 remove varTerm appTerm absTerm 886 def 32 ref appTerm 887 def appTerm refl 888 def 886 ref 873 ref appTerm betaConv appThm 87 ref 887 remove betaConv appThm 889 def 15 ref 873 ref appTerm 890 def refl appThm trans 886 remove refl 891 def 874 remove assume 892 def appThm eqMp sym 865 remove 225 ref appTerm 893 def betaConv 868 remove nil 869 remove 43 ref 893 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 870 remove 110 ref 743 remove cons nil cons cons nil cons cons 137 ref subst eqMp eqMp nil 42 ref 288 ref 28 ref 225 ref appTerm 894 def 16 ref appTerm 895 def appTerm 864 ref 21 ref 894 ref 157 ref appTerm absTerm 896 def appTerm 897 def appTerm nil cons 898 def cons 43 ref 890 ref nil cons 899 def cons nil cons 900 def cons nil cons cons 901 def 106 ref subst proveHyp 901 ref 60 ref subst 901 remove 126 ref subst nil 109 ref "n''" 2 ref var 902 def 12 ref 896 ref 902 ref varTerm 903 def appTerm 904 def appTerm 890 ref appTerm 905 def absTerm nil cons cons nil cons nil cons cons 207 ref subst 902 ref nil 73 ref 905 remove nil cons cons nil cons nil cons cons 80 ref subst nil 42 ref 904 ref nil cons 906 def cons 900 ref cons nil cons cons 907 def 60 ref subst 907 remove 126 ref subst 904 ref betaConv 904 remove assume eqMp nil 42 ref 894 remove 34 ref 903 ref appTerm 908 def appTerm 909 def nil cons 910 def cons 900 ref cons nil cons cons 911 def 106 ref subst proveHyp 911 ref 60 ref subst 911 remove 126 ref subst 44 ref "_30362" 2 ref var 912 def 15 ref 34 ref 912 remove varTerm appTerm appTerm absTerm 913 def 225 ref appTerm 914 def appTerm refl 915 def 913 ref 908 ref appTerm betaConv appThm 87 ref 914 remove betaConv appThm 916 def 15 ref 34 ref 908 ref appTerm 917 def appTerm 918 def refl appThm trans 913 remove refl 919 def 909 remove assume 920 def appThm eqMp sym 21 ref 14 ref 209 ref 903 ref appTerm 921 def 32 ref appTerm appTerm 209 ref 32 ref appTerm 922 def 917 ref appTerm appTerm absTerm 923 def 908 ref appTerm betaConv sym nil 21 ref 903 ref nil cons 924 def cons nil cons nil cons cons 925 def 21 ref 922 ref 157 ref appTerm absTerm 926 def 32 ref appTerm 927 def betaConv nil 40 ref 926 ref appTerm 928 def axiom nil 42 ref 928 remove nil cons cons 43 ref 927 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 926 remove nil cons cons 112 ref cons nil cons cons 137 ref subst eqMp eqMp 929 def subst nil 42 ref 921 ref 908 ref appTerm nil cons cons 43 ref 209 ref 908 ref appTerm 917 ref appTerm nil cons 930 def cons nil cons cons nil cons cons 126 ref subst proveHyp nil 21 ref 908 ref nil cons 931 def cons nil cons nil cons cons 929 remove subst 932 def eqMp eqMp 108 ref 109 ref 923 ref nil cons cons 110 ref 931 ref cons nil cons cons nil cons cons 732 remove sym nil 261 ref 86 ref 12 ref 712 remove appTerm 90 remove appTerm 933 def absTerm nil cons cons nil cons nil cons cons 272 remove 198 ref subst 934 def subst 86 ref nil 73 ref 933 remove nil cons cons nil cons nil cons cons 80 ref subst 724 ref 60 ref subst 724 remove 126 ref subst nil 384 remove 722 remove cons nil cons cons 106 ref subst 711 ref 122 ref appTerm 935 def betaConv nil 714 remove 43 ref 935 remove nil cons cons nil cons cons nil cons cons 106 ref subst 678 ref 117 ref 711 remove nil cons cons 121 ref 612 remove cons nil cons cons nil cons cons 137 ref subst eqMp eqMp eqMp eqMp nil 738 remove 737 remove cons nil cons cons 99 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp 936 def subst proveHyp nil 42 ref 864 ref 923 remove appTerm nil cons cons 43 ref 921 ref 917 ref appTerm nil cons 937 def cons nil cons cons nil cons cons 106 ref subst proveHyp nil "p" 2 ref var 938 def 917 ref nil cons cons 152 ref 924 ref cons nil cons cons nil cons cons 938 ref 12 ref 864 ref 21 ref 14 ref 211 ref appTerm 922 ref 938 ref varTerm 939 def appTerm 940 def appTerm 941 def absTerm 942 def appTerm 943 def appTerm 944 def 210 ref 939 ref appTerm 945 def appTerm 946 def absTerm 947 def 939 ref appTerm 948 def betaConv 152 ref 40 ref 947 ref appTerm 949 def absTerm 950 def 155 ref appTerm 951 def betaConv nil 40 ref 152 ref 40 ref 21 ref 40 ref 938 ref 12 ref 941 ref appTerm 945 ref appTerm absTerm 952 def appTerm 953 def absTerm 954 def appTerm 955 def absTerm 956 def appTerm 957 def axiom nil 42 ref 957 ref nil cons 958 def cons 959 def 43 ref 40 ref 950 ref appTerm nil cons 960 def cons nil cons cons nil cons cons 961 def 106 ref subst proveHyp 961 ref 60 ref subst 961 remove 126 ref subst nil 109 ref 950 remove nil cons cons 962 def nil cons nil cons cons 207 ref subst 152 ref nil 73 ref 949 remove nil cons 963 def cons nil cons nil cons cons 80 ref subst nil 109 ref 947 remove nil cons cons 964 def nil cons nil cons cons 207 ref subst 938 ref nil 73 ref 946 remove nil cons cons nil cons nil cons cons 80 ref subst nil 42 ref 943 remove nil cons 965 def cons 966 def 43 ref 945 ref nil cons 967 def cons nil cons 968 def cons nil cons cons 969 def 60 ref subst 969 remove 126 ref subst nil 959 ref 968 ref cons nil cons cons 970 def 106 ref subst nil 966 remove 43 ref 12 ref 957 remove appTerm 945 remove appTerm 971 def nil cons 972 def cons nil cons 973 def cons nil cons cons 106 ref subst nil 109 ref 21 ref 12 ref 942 ref 32 ref appTerm 974 def appTerm 971 ref appTerm 975 def absTerm nil cons cons nil cons nil cons cons 207 ref subst 21 ref nil 73 ref 975 remove nil cons cons nil cons nil cons cons 80 ref subst nil 42 ref 974 ref nil cons 976 def cons 973 ref cons nil cons cons 977 def 60 ref subst 977 remove 126 ref subst 974 ref betaConv 974 remove assume eqMp nil 42 ref 941 remove nil cons 978 def cons 979 def 973 remove cons nil cons cons 980 def 106 ref subst proveHyp 980 ref 60 ref subst 980 remove 126 ref subst 970 ref 60 ref subst 970 remove 126 ref subst nil 979 remove 968 remove cons nil cons cons 106 ref subst 952 ref 939 ref appTerm 981 def betaConv 954 ref 32 ref appTerm 982 def betaConv 956 ref 155 ref appTerm 983 def betaConv nil 959 remove 43 ref 983 remove nil cons cons nil cons cons nil cons cons 106 ref subst 108 ref 109 ref 956 remove nil cons cons 167 ref cons nil cons cons 137 ref subst eqMp eqMp nil 42 ref 955 remove nil cons cons 43 ref 982 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 954 remove nil cons cons 112 ref cons nil cons cons 137 ref subst eqMp eqMp nil 42 ref 953 remove nil cons cons 43 ref 981 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 952 remove nil cons cons 110 ref 939 ref nil cons 984 def cons nil cons 985 def cons nil cons cons 137 ref subst eqMp eqMp eqMp eqMp nil 85 ref 958 remove cons 986 def 86 ref 967 remove cons nil cons 987 def cons nil cons cons 99 ref subst deductAntisym eqMp eqMp nil 85 ref 978 remove cons 86 ref 972 remove cons nil cons 988 def cons nil cons cons 99 ref subst deductAntisym eqMp eqMp eqMp nil 85 ref 976 remove cons 988 ref cons nil cons cons 99 ref subst deductAntisym eqMp eqMp absThm eqMp nil 42 ref 40 ref 110 ref 12 ref 942 ref 110 ref varTerm 989 def appTerm appTerm 971 ref appTerm absTerm appTerm nil cons cons 43 ref 944 remove 971 remove appTerm nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 942 remove nil cons cons 988 remove cons nil cons cons 739 ref subst eqMp eqMp eqMp eqMp nil 85 ref 965 remove cons 987 remove cons nil cons cons 99 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp nil 986 remove 86 ref 960 ref cons nil cons cons nil cons cons 99 ref subst deductAntisym eqMp eqMp nil 42 ref 960 remove cons 43 ref 951 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 962 remove 167 ref cons nil cons cons 137 ref subst eqMp eqMp nil 42 ref 963 remove cons 43 ref 948 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 964 remove 985 ref cons nil cons cons 137 ref subst eqMp eqMp subst eqMp nil 42 ref 937 remove cons 43 ref 15 ref 903 remove appTerm 990 def nil cons 991 def cons nil cons cons nil cons cons 106 ref subst proveHyp nil "n'''" 2 ref var 992 def 924 remove cons nil cons nil cons cons 992 ref 12 ref 209 ref 992 ref varTerm 993 def appTerm 917 remove appTerm appTerm 15 ref 993 ref appTerm appTerm absTerm 994 def 993 ref appTerm 995 def betaConv 44 ref "_30370" 2 ref var 996 def 40 ref 902 ref 12 ref 921 ref 34 ref 996 remove varTerm appTerm appTerm appTerm 990 ref appTerm absTerm appTerm absTerm 997 def 225 ref appTerm 998 def appTerm refl 997 ref 908 ref appTerm betaConv appThm 87 ref 998 remove betaConv appThm 40 ref 994 ref appTerm 999 def refl appThm trans 997 remove refl 920 remove appThm eqMp 44 ref "_30350" 2 ref var 1000 def 40 ref 224 ref 12 ref 859 ref 1000 remove varTerm appTerm appTerm 741 ref appTerm absTerm appTerm absTerm 1001 def 32 ref appTerm 1002 def appTerm refl 1001 ref 873 ref appTerm betaConv appThm 87 ref 1002 remove betaConv appThm 40 ref 902 remove 12 ref 921 remove 873 remove appTerm appTerm 990 ref appTerm absTerm appTerm refl appThm trans 1001 remove refl 892 remove appThm eqMp 860 remove assume eqMp eqMp nil 42 ref 999 remove nil cons cons 43 ref 995 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 994 remove nil cons cons 110 ref 993 remove nil cons cons nil cons cons nil cons cons 137 ref subst eqMp eqMp 1003 def subst eqMp nil 42 ref 991 remove cons 43 ref 15 ref 908 remove appTerm 1004 def nil cons cons nil cons 1005 def cons nil cons cons 126 ref subst proveHyp 932 remove nil 42 ref 930 remove cons 1005 remove cons nil cons cons 106 ref subst proveHyp nil 992 remove 931 remove cons nil cons nil cons cons 1003 remove subst eqMp eqMp nil 42 ref 14 ref 990 remove appTerm 1004 remove appTerm nil cons cons 43 ref 918 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 925 remove 191 ref 32 ref appTerm 1006 def betaConv nil 42 ref 204 remove cons 43 ref 1006 remove nil cons cons nil cons cons nil cons cons 106 ref subst 108 ref 109 ref 191 remove nil cons cons 112 ref cons nil cons cons 137 ref subst eqMp eqMp subst eqMp eqMp eqMp nil 85 ref 910 remove cons 86 ref 899 ref cons nil cons 1007 def cons nil cons cons 99 ref subst deductAntisym eqMp eqMp eqMp nil 85 ref 906 remove cons 1007 ref cons nil cons cons 99 ref subst deductAntisym eqMp eqMp absThm eqMp nil 42 ref 40 ref 110 ref 12 ref 896 ref 989 ref appTerm appTerm 890 ref appTerm absTerm appTerm nil cons cons 43 ref 12 ref 897 ref appTerm 890 remove appTerm nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 896 remove nil cons cons 1007 ref cons nil cons cons 739 ref subst eqMp nil 42 ref 895 ref nil cons 1008 def cons 900 remove cons nil cons cons 1009 def 60 ref subst 1009 remove 126 ref subst 915 remove "_30352" 2 ref var 1010 def 15 ref 34 ref 1010 remove varTerm appTerm appTerm absTerm 16 ref appTerm betaConv appThm 916 remove 189 ref refl appThm trans 919 remove 895 remove assume appThm eqMp sym 189 remove assume eqMp eqMp nil 85 ref 1008 remove cons 1011 def 1007 ref cons nil cons cons 99 ref subst deductAntisym eqMp nil 1011 remove 86 ref 897 remove nil cons cons 365 ref 899 remove cons nil cons cons cons nil cons cons 381 ref subst proveHyp proveHyp eqMp nil 85 ref 898 remove cons 1007 remove cons nil cons cons 99 ref subst deductAntisym eqMp eqMp eqMp eqMp nil 85 ref 883 remove cons 86 ref 208 ref cons 1012 def nil cons 1013 def cons nil cons cons 99 ref subst deductAntisym eqMp eqMp eqMp nil 85 ref 881 remove cons 1013 ref cons nil cons cons 99 ref subst deductAntisym eqMp eqMp absThm eqMp nil 42 ref 40 ref 110 ref 12 ref 875 ref 989 ref appTerm appTerm 145 ref appTerm absTerm appTerm nil cons cons 43 ref 12 ref 876 ref appTerm 145 ref appTerm nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 875 remove nil cons cons 1013 ref cons nil cons cons 739 ref subst eqMp nil 42 ref 872 ref nil cons 1014 def cons 862 ref cons nil cons cons 1015 def 60 ref subst 1015 remove 126 ref subst 888 remove "_30332" 2 ref var 1016 def 15 ref 1016 remove varTerm appTerm absTerm 16 ref appTerm betaConv appThm 889 remove 17 ref refl appThm trans 891 remove 872 remove assume appThm eqMp sym 17 remove assume eqMp eqMp nil 85 ref 1014 remove cons 1017 def 1013 ref cons nil cons cons 99 ref subst deductAntisym eqMp nil 1017 remove 86 ref 876 remove nil cons cons 365 ref 208 remove cons nil cons cons cons nil cons cons 381 ref subst proveHyp proveHyp eqMp nil 85 ref 877 remove cons 1013 ref cons nil cons cons 99 ref subst deductAntisym eqMp eqMp eqMp nil 85 ref 861 remove cons 1013 ref cons nil cons cons 99 ref subst deductAntisym eqMp eqMp eqMp absThm eqMp nil 42 ref 40 ref 218 remove appTerm nil cons cons 862 ref cons nil cons cons 106 ref subst proveHyp 13 ref 87 ref 144 ref "_30331" 2 ref var 1018 def 13 ref 1018 ref 40 ref 152 ref 12 ref 210 remove 1018 ref varTerm 1019 def appTerm appTerm 1020 def 216 remove appTerm absTerm appTerm 1021 def absTerm 1022 def 1019 ref appTerm betaConv appThm 1023 def 144 ref 21 ref 1018 ref 21 ref 12 ref 28 ref 1019 ref appTerm 32 ref appTerm appTerm 145 ref appTerm 1024 def absTerm 1025 def absTerm 1026 def 1019 ref appTerm betaConv 223 ref appThm 1025 ref 32 ref appTerm betaConv trans 1027 def absThm appThm appThm absThm appThm appThm 144 ref 21 ref 144 ref 1018 ref 1023 ref 1027 remove appThm absThm appThm absThm appThm appThm nil 109 ref 1022 ref nil cons cons 1028 def 227 remove 1026 remove nil cons cons nil cons cons nil cons cons 740 remove subst eqMp 144 ref 21 ref 87 ref 144 ref 1018 ref 1023 remove 1024 remove refl appThm absThm appThm appThm 13 ref 1022 remove 32 ref appTerm betaConv appThm 858 ref appThm appThm nil 1028 remove 1012 remove 742 remove 111 ref cons nil cons cons cons nil cons cons 857 remove subst eqMp absThm appThm trans appThm 858 remove appThm nil 42 ref 40 ref 1018 ref 12 ref 1021 remove appTerm 40 ref 1025 remove appTerm 1029 def appTerm absTerm appTerm nil cons 1030 def cons 1031 def 862 ref cons nil cons cons 1032 def 60 ref subst 1032 remove 126 ref subst 223 ref nil 42 ref 871 ref 32 ref appTerm nil cons cons 862 remove cons nil cons cons 106 ref subst proveHyp 224 ref 12 ref 871 ref 225 ref appTerm appTerm 741 remove appTerm absTerm 1033 def 32 ref appTerm 1034 def betaConv 1018 ref 1029 remove absTerm 1035 def 32 ref appTerm 1036 def betaConv nil 1031 remove 43 ref 40 ref 1035 ref appTerm nil cons 1037 def cons nil cons cons nil cons cons 106 ref subst 13 ref 144 ref 1018 ref 13 ref 144 ref 152 ref 1020 remove refl 1035 ref 155 ref appTerm betaConv appThm absThm appThm appThm 1035 ref 1019 remove appTerm betaConv 1038 def appThm absThm appThm appThm 144 ref 1018 remove 1038 remove absThm appThm appThm nil 8 ref 1035 remove nil cons 1039 def cons nil cons nil cons cons 8 ref 12 ref 40 ref 21 ref 12 ref 40 ref 152 ref 212 remove 15 ref 155 ref appTerm appTerm absTerm appTerm appTerm 145 ref appTerm absTerm appTerm appTerm 187 ref appTerm absTerm 1040 def 15 ref appTerm 1041 def betaConv nil 7 ref 1040 ref appTerm 1042 def axiom nil 42 ref 1042 remove nil cons cons 43 ref 1041 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 196 ref 188 ref 1040 remove nil cons cons "x" 5 remove var 15 ref nil cons cons nil cons 1043 def cons nil cons cons 137 ref subst eqMp eqMp subst eqMp eqMp nil 42 ref 1037 remove cons 43 ref 1036 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 1039 remove cons 112 ref cons nil cons cons 137 ref subst eqMp eqMp nil 42 ref 40 ref 1033 ref appTerm nil cons cons 43 ref 1034 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 1033 remove nil cons cons 112 ref cons nil cons cons 137 ref subst eqMp eqMp eqMp eqMp nil 85 ref 1030 remove cons 1013 remove cons nil cons cons 99 ref subst deductAntisym eqMp eqMp eqMp eqMp absThm eqMp proveHyp proveHyp proveHyp proveHyp eqMp nil 85 ref 199 remove cons 86 ref 200 remove cons nil cons cons nil cons cons 99 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp 1044 def nil 7 ref 8 ref 12 ref 18 ref 14 ref 15 ref 31 remove 16 ref appTerm 1045 def appTerm appTerm 40 ref 21 ref 12 ref 146 remove 15 ref 150 ref 1045 ref appTerm 1046 def appTerm appTerm appTerm 15 ref 150 ref 35 remove 1045 ref appTerm 1047 def appTerm 1048 def appTerm appTerm absTerm appTerm appTerm appTerm appTerm 187 ref appTerm absTerm 1049 def appTerm 1050 def thm nil "P" 1 ref 30 ref 4 ref cons opType 1051 def var 1052 def "f" 30 ref var 1053 def 0 ref 1 ref 1051 remove 4 ref cons opType 1054 def constTerm 1055 def "g" 30 ref var 1056 def 40 ref 21 ref 12 ref 40 ref 152 ref 12 ref 288 ref 28 ref 156 ref 1045 ref appTerm 1057 def appTerm 1058 def 32 ref appTerm appTerm 28 ref 156 ref 1047 ref appTerm appTerm 1059 def 32 ref appTerm appTerm appTerm 1060 def 28 ref 1053 ref varTerm 1061 def 155 ref appTerm appTerm 1056 ref varTerm 1062 def 155 ref appTerm appTerm 1063 def appTerm absTerm appTerm appTerm 1064 def 28 ref "f'" 30 ref var 1065 def 224 ref "Data.Bool.cond" const 1066 def 1 ref 3 ref 148 ref nil cons cons opType constTerm 1067 def 859 remove 1047 ref appTerm appTerm 225 ref appTerm 1068 def 149 ref 1065 remove varTerm 1069 def "Number.Natural.-" const 148 remove constTerm 1070 def 225 remove appTerm 1071 def 1045 ref appTerm 1072 def appTerm appTerm 1069 remove 1071 remove 1047 ref appTerm 1073 def appTerm appTerm appTerm absTerm absTerm 1074 def 1061 ref appTerm 1075 def 32 ref appTerm 1076 def appTerm 1074 ref 1062 ref appTerm 1077 def 32 ref appTerm appTerm appTerm absTerm appTerm 1078 def absTerm 1079 def appTerm 1080 def absTerm 1081 def nil cons cons nil cons nil cons cons "A" 147 ref cons nil cons 1082 def 197 ref cons 198 ref subst 1083 def subst 1053 ref nil 73 ref 1080 remove nil cons cons nil cons nil cons cons 80 ref subst nil 1052 ref 1079 remove nil cons cons nil cons nil cons cons 1083 ref subst 1056 remove nil 73 ref 1078 remove nil cons cons nil cons nil cons cons 80 ref subst 144 ref 21 ref 1064 ref refl 28 ref refl 1084 def 1075 remove betaConv 223 ref appThm 224 ref 1068 ref 149 ref 1061 ref 1072 ref appTerm appTerm 1061 ref 1073 ref appTerm appTerm appTerm absTerm 32 ref appTerm betaConv trans 1085 def appThm 1077 remove betaConv 223 ref appThm 224 remove 1068 remove 149 ref 1062 ref 1072 remove appTerm appTerm 1062 ref 1073 remove appTerm appTerm appTerm absTerm 32 ref appTerm betaConv trans appThm appThm absThm appThm sym nil 42 ref 40 ref 152 ref 12 ref 288 ref 1058 ref 16 ref appTerm appTerm 1059 ref 16 ref appTerm appTerm appTerm 1063 ref appTerm absTerm appTerm 1086 def nil cons 1087 def cons 43 ref 28 ref 1067 ref 209 ref 16 ref appTerm 1047 ref appTerm appTerm 16 ref appTerm 1088 def 149 ref 1061 ref 1070 ref 16 ref appTerm 1089 def 1045 ref appTerm 1090 def appTerm appTerm 1061 ref 1089 remove 1047 ref appTerm 1091 def appTerm appTerm 1092 def appTerm appTerm 1088 remove 149 ref 1062 ref 1090 remove appTerm appTerm 1062 ref 1091 remove appTerm appTerm 1093 def appTerm appTerm 1094 def nil cons 1095 def cons nil cons cons nil cons cons 1096 def 60 ref subst 1096 remove 126 ref subst 1084 ref 1067 ref refl 1097 def 139 ref 24 ref nil 152 ref 33 ref nil cons 1098 def cons nil cons nil cons cons 173 remove subst subst appThm 24 ref 21 ref 28 ref 34 ref 33 ref appTerm appTerm 176 remove appTerm absTerm 1099 def 32 ref appTerm 1100 def betaConv 19 ref 144 ref 21 ref nil 110 ref 157 ref nil cons 1101 def cons nil cons nil cons cons 206 ref 276 remove subst 1102 def subst absThm appThm 409 ref 206 ref 777 remove subst subst 1103 def trans appThm 19 ref 28 ref 183 ref appTerm 1104 def refl 143 ref appThm nil 110 ref 184 remove cons nil cons nil cons cons 1102 ref subst trans appThm 19 ref 144 ref 21 ref 1084 ref 139 ref 21 ref 28 ref 36 remove appTerm 150 ref 32 ref appTerm 1105 def appTerm 1106 def absTerm 1107 def 32 ref appTerm 1108 def betaConv 1109 def 1084 ref 141 remove appThm 24 ref 21 ref 28 ref 149 ref 16 ref appTerm 1110 def 32 ref appTerm appTerm 32 ref appTerm absTerm 1111 def 32 ref appTerm 1112 def betaConv nil 40 ref 1111 ref appTerm 1113 def axiom nil 42 ref 1113 remove nil cons cons 43 ref 1112 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 1111 remove nil cons cons 112 ref cons nil cons cons 137 ref subst eqMp eqMp 1114 def subst appThm nil 110 ref 22 ref cons nil cons nil cons cons 1102 ref subst 1115 def trans sym 79 ref eqMp nil 42 ref 140 remove 1110 ref 16 ref appTerm appTerm 1116 def nil cons cons 43 ref 40 ref 21 ref 12 ref 1106 ref appTerm 177 remove 149 ref 157 ref appTerm 157 ref appTerm appTerm 1117 def appTerm 1118 def absTerm 1119 def appTerm 1120 def nil cons cons nil cons cons nil cons cons 126 ref subst proveHyp nil 109 ref 1119 remove nil cons cons nil cons nil cons cons 207 ref subst 21 ref nil 73 ref 1118 remove nil cons cons nil cons nil cons cons 80 ref subst nil 42 ref 1106 ref nil cons 1121 def cons 43 ref 1117 remove nil cons 1122 def cons nil cons cons nil cons cons 1123 def 60 ref subst 1123 remove 126 ref subst 1084 ref 181 remove 139 ref 139 ref 1106 remove assume appThm appThm trans appThm nil 21 ref 1101 remove cons 1124 def 154 ref cons nil cons cons 21 ref 28 ref 149 ref 34 ref 155 ref appTerm 1125 def appTerm 32 ref appTerm appTerm 159 ref appTerm absTerm 1126 def 32 ref appTerm 1127 def betaConv 152 ref 40 ref 1126 ref appTerm 1128 def absTerm 1129 def 155 ref appTerm 1130 def betaConv nil 40 ref 1129 ref appTerm 1131 def axiom nil 42 ref 1131 remove nil cons cons 43 ref 1130 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 1129 remove nil cons cons 167 ref cons nil cons cons 137 ref subst eqMp eqMp nil 42 ref 1128 remove nil cons cons 43 ref 1127 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 1126 remove nil cons cons 112 ref cons nil cons cons 137 ref subst eqMp eqMp subst 1132 def 139 ref 169 ref 168 ref subst appThm 1133 def trans appThm nil 110 ref 34 ref 34 ref 1105 remove appTerm 1134 def appTerm nil cons cons nil cons nil cons cons 1102 ref subst 1135 def trans sym 79 ref eqMp eqMp nil 85 ref 1121 remove cons 86 ref 1122 remove cons nil cons cons nil cons cons 99 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp nil 42 ref 14 ref 1116 remove appTerm 1120 remove appTerm nil cons cons 43 ref 40 ref 1107 ref appTerm nil cons 1136 def cons nil cons cons nil cons cons 106 ref subst proveHyp 13 ref 19 ref 1107 ref 16 ref appTerm betaConv appThm 144 ref 21 ref 13 ref 1109 ref appThm 1107 ref 157 ref appTerm betaConv appThm absThm appThm appThm appThm 144 ref 21 ref 1109 remove absThm appThm appThm nil 8 ref 1107 remove nil cons 1137 def cons nil cons nil cons cons 8 ref 12 ref 18 remove 40 ref 21 ref 12 ref 145 remove appTerm 190 remove appTerm absTerm appTerm appTerm appTerm 187 remove appTerm absTerm 1138 def 15 ref appTerm 1139 def betaConv nil 7 remove 1138 ref appTerm 1140 def axiom nil 42 ref 1140 remove nil cons cons 43 ref 1139 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 196 ref 188 ref 1138 remove nil cons cons 1043 ref cons nil cons cons 137 ref subst eqMp eqMp subst eqMp eqMp nil 42 ref 1136 remove cons 43 ref 1108 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 1137 remove cons 112 ref cons nil cons cons 137 ref subst eqMp eqMp 1141 def appThm 1142 def appThm 138 remove 1142 remove trans 1143 def appThm nil 110 ref 1134 remove nil cons cons nil cons nil cons cons 1102 ref subst trans absThm appThm 1103 ref trans appThm 144 ref 21 ref 1084 ref 139 ref 1143 remove appThm appThm nil 1124 ref nil cons nil cons cons 1144 def 1141 remove subst 1132 remove trans 1133 remove trans appThm 1135 remove trans absThm appThm 1103 remove trans appThm 409 remove 324 remove subst 1145 def trans appThm 1145 ref trans appThm 1145 remove trans sym 79 ref eqMp nil 85 ref 40 ref 21 ref 28 ref 157 ref appTerm 157 ref appTerm absTerm appTerm nil cons cons 86 ref 14 ref 1104 remove 1045 ref appTerm 1146 def appTerm 14 ref 40 ref 21 ref 28 ref 37 remove appTerm 33 remove appTerm absTerm appTerm 1147 def appTerm 40 ref 1099 ref appTerm 1148 def appTerm 1149 def appTerm nil cons cons nil cons cons nil cons cons 203 ref subst proveHyp 1150 def nil 85 ref 1146 remove nil cons cons 86 ref 1149 remove nil cons cons nil cons cons nil cons cons 1151 def 203 ref subst proveHyp nil 85 ref 1147 remove nil cons cons 86 ref 1148 remove nil cons 1152 def cons nil cons cons nil cons cons 203 ref subst proveHyp nil 42 ref 1152 remove cons 43 ref 1100 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 1099 remove nil cons cons 112 ref cons nil cons cons 137 ref subst eqMp eqMp subst 175 remove 1150 remove 1151 remove 99 ref subst proveHyp appThm trans 1153 def trans 1154 def nil 152 ref 1045 ref nil cons 1155 def cons 23 remove 938 ref 1047 ref nil cons 1156 def cons 1157 def nil cons 1158 def cons cons nil cons cons nil 42 ref 28 ref 159 ref appTerm 1159 def 939 ref appTerm 1160 def nil cons 1161 def cons 1162 def 43 ref 44 ref 940 ref appTerm 65 ref appTerm nil cons cons nil cons cons nil cons cons 106 ref subst 12 ref 1160 ref appTerm 1163 def refl nil 73 ref 940 remove nil cons cons nil cons nil cons cons 73 ref 44 ref 78 remove appTerm 76 ref appTerm absTerm 1164 def 76 ref appTerm 1165 def betaConv nil 258 ref 1164 ref appTerm 1166 def axiom nil 42 ref 1166 remove nil cons cons 43 ref 1165 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 260 ref 261 ref 1164 remove nil cons cons 264 ref cons nil cons cons 137 ref subst eqMp eqMp subst nil 21 ref 984 remove cons 154 ref cons nil cons cons 21 ref 44 ref 211 ref appTerm 1167 def 864 ref "d" 2 ref var 1168 def 871 remove 156 ref 34 ref 1168 ref varTerm 1169 def appTerm appTerm appTerm absTerm appTerm appTerm absTerm 1170 def 32 ref appTerm 1171 def betaConv 152 ref 40 ref 1170 ref appTerm 1172 def absTerm 1173 def 155 ref appTerm 1174 def betaConv nil 40 ref 1173 ref appTerm 1175 def axiom nil 42 ref 1175 remove nil cons cons 43 ref 1174 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 1173 remove nil cons cons 167 ref cons nil cons cons 137 ref subst eqMp eqMp nil 42 ref 1172 remove nil cons cons 43 ref 1171 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 1170 remove nil cons cons 112 ref cons nil cons cons 137 ref subst eqMp eqMp subst trans 864 ref refl 1168 ref 1084 ref 939 ref refl appThm nil 21 ref 1169 ref nil cons cons 154 ref cons nil cons cons 168 ref subst appThm absThm appThm trans appThm sym nil 42 ref 1163 remove 864 remove 1168 ref 28 ref 939 ref appTerm 34 ref 150 ref 1169 ref appTerm appTerm appTerm 1176 def absTerm 1177 def appTerm 1178 def appTerm 1179 def nil cons cons nil cons nil cons cons 278 remove subst sym nil 42 ref 250 ref 1179 remove appTerm 1180 def nil cons 1181 def cons 282 ref cons nil cons cons 1182 def 60 ref subst 1182 remove 126 ref subst nil 40 ref 152 ref 40 ref 21 ref 28 ref 158 ref appTerm 1183 def 150 ref 155 ref appTerm 1184 def appTerm 1185 def absTerm appTerm absTerm 1186 def appTerm 1187 def axiom nil 42 ref 1187 remove nil cons 1188 def cons 1189 def 282 ref cons nil cons cons 1190 def 106 ref subst proveHyp 1190 ref 60 ref subst 1190 remove 126 ref subst nil "_2184" 2 ref var 1191 def 111 remove cons "_2183" 2 ref var 1192 def 166 ref cons nil cons cons nil cons cons 21 ref 28 ref 149 ref 1192 remove varTerm 1193 def appTerm 32 ref appTerm appTerm 150 ref 1193 ref appTerm appTerm absTerm 1194 def 1191 remove varTerm 1195 def appTerm 1196 def betaConv 1186 ref 1193 ref appTerm 1197 def betaConv nil 1189 remove 43 ref 1197 remove nil cons cons nil cons cons nil cons cons 106 ref subst 108 ref 109 ref 1186 remove nil cons cons 110 ref 1193 remove nil cons cons nil cons cons nil cons cons 137 ref subst eqMp eqMp nil 42 ref 40 ref 1194 ref appTerm nil cons cons 43 ref 1196 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 1194 remove nil cons cons 110 ref 1195 remove nil cons cons nil cons cons nil cons cons 137 ref subst eqMp eqMp subst nil 42 ref 1185 remove nil cons cons 43 ref 1159 ref 34 ref 1184 ref appTerm appTerm nil cons 1198 def cons nil cons cons nil cons cons 106 ref subst proveHyp nil "_9249" 2 ref var 1199 def 1184 remove nil cons cons "_9248" 2 ref var 1200 def 158 ref nil cons cons nil cons cons nil cons cons nil 42 ref 28 ref 1200 remove varTerm 1201 def appTerm 1199 remove varTerm 1202 def appTerm 1203 def nil cons 1204 def cons 43 ref 28 ref 34 ref 1201 remove appTerm appTerm 34 ref 1202 remove appTerm appTerm nil cons 1205 def cons nil cons cons nil cons cons 1206 def 60 ref subst 1206 remove 126 ref subst 139 ref 1203 remove assume appThm eqMp nil 85 ref 1204 remove cons 86 ref 1205 remove cons nil cons cons nil cons cons 99 ref subst deductAntisym eqMp subst eqMp nil 42 ref 1198 remove cons 282 remove cons nil cons cons 106 ref subst proveHyp nil "_9241" 2 ref var 1207 def 166 remove cons nil cons nil cons cons nil 42 ref 1159 remove 34 ref 150 ref 1207 remove varTerm 1208 def appTerm appTerm 1209 def appTerm 1210 def nil cons cons nil cons nil cons cons 680 remove subst 44 ref "_9246" 2 ref var 1211 def 250 ref 28 ref 1211 remove varTerm appTerm 1209 remove appTerm appTerm absTerm 1212 def 939 ref appTerm 1213 def appTerm refl 1212 ref 159 remove appTerm betaConv appThm 87 ref 1213 remove betaConv appThm 250 ref 1210 remove appTerm refl appThm trans 1212 remove refl nil 1162 remove 43 ref 1178 remove nil cons cons nil cons cons nil cons cons 482 remove subst 19 ref 1160 remove refl appThm nil 109 ref 1177 ref nil cons cons nil cons nil cons cons 206 ref 87 ref 306 ref 465 remove 444 remove appThm appThm appThm 116 ref 448 remove appTerm refl appThm sym 449 remove 128 remove 44 ref 250 ref 526 remove appTerm appTerm 116 ref 452 remove appTerm appTerm absTerm 1214 def 129 remove appTerm 1215 def betaConv nil 455 remove 1214 ref appTerm 1216 def axiom nil 42 ref 1216 remove nil cons cons 43 ref 1215 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 457 remove 458 remove 1214 remove nil cons cons 460 remove cons nil cons cons 137 ref subst eqMp eqMp subst eqMp subst subst 144 ref 1168 ref 306 remove 1177 remove 1169 remove appTerm betaConv appThm absThm appThm trans appThm trans 1180 remove assume eqMp 1217 def nil 85 ref 1161 remove cons 86 ref 40 ref 1168 remove 250 ref 1176 remove appTerm absTerm 1218 def appTerm nil cons 1219 def cons nil cons cons nil cons cons 1220 def 99 ref subst proveHyp sym appThm eqMp 1218 ref 1208 ref appTerm 1221 def betaConv 1217 remove 1220 remove 203 remove subst proveHyp nil 42 ref 1219 remove cons 43 ref 1221 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 1218 remove nil cons cons 110 ref 1208 remove nil cons cons nil cons cons nil cons cons 137 ref subst eqMp eqMp eqMp eqMp subst eqMp eqMp nil 85 ref 1188 remove cons 681 ref cons nil cons cons 99 ref subst deductAntisym eqMp eqMp eqMp nil 85 ref 1181 remove cons 681 remove cons nil cons cons 99 ref subst deductAntisym eqMp eqMp eqMp eqMp 1222 def subst deductAntisym 1154 remove eqMp appThm 16 ref refl 1223 def appThm 1224 def 1092 ref refl appThm nil "t2" 2 ref var 1225 def 1092 remove nil cons cons "t1" 2 ref var 1226 def 22 ref cons nil cons 1227 def cons nil cons cons 206 ref "t2" 113 ref var 1228 def 275 ref 1066 remove 1 ref 3 ref 1 ref 113 ref 1 ref 113 ref 429 ref cons opType nil cons cons opType nil cons cons opType constTerm 1229 def 65 ref appTerm "t1" 113 ref var 1230 def varTerm 1231 def appTerm 1228 ref varTerm 1232 def appTerm appTerm 1231 ref appTerm absTerm 1233 def 1232 ref appTerm 1234 def betaConv 1230 ref 116 ref 1233 ref appTerm 1235 def absTerm 1236 def 1231 ref appTerm 1237 def betaConv nil 116 ref 1236 ref appTerm 1238 def axiom nil 42 ref 1238 remove nil cons cons 43 ref 1237 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 678 ref 117 ref 1236 remove nil cons cons 121 ref 1231 ref nil cons cons nil cons 1239 def cons nil cons cons 137 ref subst eqMp eqMp nil 42 ref 1235 remove nil cons cons 43 ref 1234 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 678 ref 117 ref 1233 remove nil cons cons 121 ref 1232 ref nil cons cons nil cons 1240 def cons nil cons cons 137 ref subst eqMp eqMp subst 1241 def subst trans 1242 def appThm 1224 remove 1093 ref refl appThm nil 1225 ref 1093 remove nil cons cons 1227 remove cons nil cons cons 1241 ref subst trans appThm 1115 remove trans sym 79 ref eqMp eqMp nil 85 ref 1087 remove cons 86 ref 1095 remove cons nil cons cons nil cons cons 99 ref subst deductAntisym eqMp nil 42 ref 12 ref 1086 remove appTerm 1094 remove appTerm 1243 def nil cons cons 43 ref 14 ref 12 ref 40 ref 152 ref 12 ref 288 ref 1058 ref 1045 ref appTerm appTerm 1059 ref 1045 ref appTerm appTerm appTerm 1063 ref appTerm absTerm appTerm 1244 def appTerm 28 ref 1067 ref 209 ref 1045 ref appTerm 1047 ref appTerm appTerm 1045 ref appTerm 1245 def 149 ref 1061 ref 1070 ref 1045 ref appTerm 1246 def 1045 ref appTerm 1247 def appTerm appTerm 1061 ref 1246 remove 1047 ref appTerm 1248 def appTerm 1249 def appTerm appTerm appTerm 1245 remove 149 ref 1062 ref 1247 ref appTerm appTerm 1062 ref 1248 remove appTerm 1250 def appTerm appTerm appTerm 1251 def appTerm 1252 def appTerm 40 ref 21 ref 12 ref 14 ref 1064 remove 28 ref 1067 ref 922 remove 1047 ref appTerm appTerm 32 ref appTerm 1253 def 149 ref 1061 ref 1070 ref 32 ref appTerm 1254 def 1045 ref appTerm 1255 def appTerm appTerm 1061 ref 1254 remove 1047 ref appTerm 1256 def appTerm appTerm appTerm 1257 def appTerm 1253 remove 149 ref 1062 ref 1255 remove appTerm appTerm 1062 ref 1256 remove appTerm appTerm appTerm appTerm appTerm 1258 def appTerm 12 ref 40 ref 152 ref 12 ref 288 ref 1058 ref 1046 ref appTerm appTerm 1059 ref 1046 ref appTerm appTerm appTerm 1063 ref appTerm absTerm appTerm appTerm 28 ref 1067 ref 209 ref 1046 ref appTerm 1047 ref appTerm appTerm 1046 ref appTerm 1259 def 149 ref 1061 ref 1070 ref 1046 ref appTerm 1260 def 1045 ref appTerm 1261 def appTerm appTerm 1061 ref 1260 remove 1047 ref appTerm 1262 def appTerm appTerm appTerm appTerm 1259 remove 149 ref 1062 ref 1261 remove appTerm appTerm 1062 ref 1262 remove appTerm appTerm appTerm appTerm appTerm appTerm 1263 def appTerm 12 ref 40 ref 152 ref 12 ref 288 ref 1058 ref 1048 ref appTerm appTerm 1059 ref 1048 ref appTerm appTerm appTerm 1063 remove appTerm absTerm 1264 def appTerm 1265 def appTerm 28 ref 1067 ref 209 ref 1048 ref appTerm 1047 ref appTerm 1266 def appTerm 1048 ref appTerm 1267 def 149 ref 1061 ref 1070 ref 1048 ref appTerm 1268 def 1045 ref appTerm 1269 def appTerm 1270 def appTerm 1271 def 1061 ref 1268 remove 1047 ref appTerm 1272 def appTerm appTerm 1273 def appTerm appTerm 1267 remove 149 ref 1062 ref 1269 ref appTerm 1274 def appTerm 1275 def 1062 ref 1272 remove appTerm appTerm 1276 def appTerm appTerm 1277 def appTerm 1278 def appTerm 1279 def absTerm 1280 def appTerm 1281 def appTerm 1282 def nil cons cons nil cons cons nil cons cons 126 ref subst proveHyp nil 42 ref 1244 remove nil cons 1283 def cons 43 ref 1251 remove nil cons 1284 def cons nil cons cons nil cons cons 1285 def 60 ref subst 1285 remove 126 ref subst 1084 ref 1097 remove 139 ref 24 ref nil 21 ref 1098 remove cons nil cons nil cons cons 1114 remove subst subst 1286 def appThm 1153 remove trans 1287 def nil 152 ref 22 remove cons 1288 def 21 ref 1155 ref cons 1289 def 1158 remove cons cons nil cons cons 1222 remove subst deductAntisym 1287 remove eqMp appThm nil 1289 ref nil cons 1290 def nil cons cons 1291 def 223 ref subst 1292 def appThm 1293 def 149 ref refl 1294 def 1061 ref refl 1295 def 1286 remove nil 42 ref 28 ref 1110 remove 1045 ref appTerm appTerm 1045 ref appTerm nil cons cons 43 ref 28 ref 1247 remove appTerm 16 ref appTerm nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp nil 1288 ref 938 ref 1155 ref cons 1290 remove cons cons nil cons cons nil 42 ref 1183 remove 939 ref appTerm 1296 def nil cons 1297 def cons 43 ref 28 ref 1070 ref 939 ref appTerm 32 ref appTerm appTerm 155 ref appTerm nil cons 1298 def cons nil cons cons nil cons cons 1299 def 60 ref subst 1299 remove 126 ref subst 44 ref "_9320" 2 ref var 1300 def 28 ref 1070 ref 1300 remove varTerm appTerm 32 ref appTerm appTerm 155 ref appTerm absTerm 1301 def 939 ref appTerm 1302 def appTerm refl 1301 ref 158 ref appTerm betaConv appThm 87 ref 1302 remove betaConv appThm 28 ref 1070 ref 158 ref appTerm 32 ref appTerm appTerm 155 ref appTerm 1303 def refl appThm trans 1301 remove refl 1296 remove assume sym appThm eqMp sym 21 ref 1303 remove absTerm 1304 def 32 ref appTerm 1305 def betaConv 152 ref 40 ref 1304 ref appTerm 1306 def absTerm 1307 def 155 ref appTerm 1308 def betaConv nil 40 ref 1307 ref appTerm 1309 def axiom nil 42 ref 1309 remove nil cons cons 43 ref 1308 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 1307 remove nil cons cons 167 ref cons nil cons cons 137 ref subst eqMp eqMp nil 42 ref 1306 remove nil cons cons 43 ref 1305 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 1304 remove nil cons cons 112 ref cons nil cons cons 137 ref subst eqMp eqMp 1310 def eqMp eqMp nil 85 ref 1297 remove cons 86 ref 1298 remove cons nil cons cons nil cons cons 99 ref subst deductAntisym eqMp subst eqMp 1311 def appThm appThm 1249 ref refl appThm appThm nil 1225 ref 149 ref 1061 ref 16 ref appTerm 1312 def appTerm 1249 remove appTerm nil cons cons 1226 ref 1155 remove cons nil cons 1313 def cons nil cons cons 1241 ref subst trans 1314 def appThm 1293 remove 1294 remove 1062 ref refl 1315 def 1311 remove appThm appThm 1250 ref refl appThm appThm nil 1225 ref 149 ref 1062 ref 16 ref appTerm appTerm 1250 remove appTerm nil cons cons 1313 remove cons nil cons cons 1241 ref subst trans appThm 1291 ref nil 112 ref nil cons cons 1102 ref subst subst trans sym 79 ref eqMp eqMp nil 85 ref 1283 remove cons 86 ref 1284 remove cons nil cons cons nil cons cons 99 ref subst deductAntisym eqMp nil 42 ref 1252 remove nil cons cons 43 ref 1281 remove nil cons cons nil cons cons nil cons cons 126 ref subst proveHyp nil 109 ref 1280 remove nil cons cons nil cons nil cons cons 207 ref subst 21 ref nil 73 ref 1279 remove nil cons cons nil cons nil cons cons 80 ref subst nil 42 ref 1263 remove nil cons 1316 def cons 43 ref 1278 remove nil cons 1317 def cons nil cons cons nil cons cons 1318 def 60 ref subst 1318 remove 126 ref subst nil 42 ref 1265 remove nil cons 1319 def cons 1320 def 43 ref 1277 remove nil cons 1321 def cons nil cons 1322 def cons nil cons cons 1323 def 60 ref subst 1323 remove 126 ref subst nil 42 ref 44 ref 1266 ref appTerm 1324 def 254 ref appTerm 1325 def nil cons 1326 def cons 1322 ref cons nil cons cons 1327 def 60 ref subst 1327 remove 126 ref subst 44 ref "_30378" 3 ref var 1328 def 28 ref 1067 ref 1328 remove varTerm appTerm 1048 ref appTerm 1329 def 1273 ref appTerm appTerm 1329 remove 1276 ref appTerm appTerm absTerm 1330 def 1266 ref appTerm 1331 def appTerm refl 1332 def 1330 ref 254 ref appTerm betaConv appThm 87 ref 1331 remove betaConv appThm 1333 def 28 ref 1067 ref 254 ref appTerm 1048 ref appTerm 1334 def 1273 ref appTerm appTerm 1335 def 1334 remove 1276 ref appTerm appTerm refl appThm trans 1330 remove refl 1336 def 1325 remove assume 1337 def appThm eqMp sym 1084 ref nil 1225 ref 1273 ref nil cons cons 1226 remove 1048 ref nil cons 1338 def cons nil cons 1339 def cons nil cons cons 1340 def 206 ref 1228 remove 275 ref 1229 remove 254 ref appTerm 1231 ref appTerm 1232 ref appTerm appTerm 1232 ref appTerm absTerm 1341 def 1232 remove appTerm 1342 def betaConv 1230 remove 116 ref 1341 ref appTerm 1343 def absTerm 1344 def 1231 remove appTerm 1345 def betaConv nil 116 ref 1344 ref appTerm 1346 def axiom nil 42 ref 1346 remove nil cons cons 43 ref 1345 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 678 ref 117 ref 1344 remove nil cons cons 1239 remove cons nil cons cons 137 ref subst eqMp eqMp nil 42 ref 1343 remove nil cons cons 43 ref 1342 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 678 remove 117 remove 1341 remove nil cons cons 1240 remove cons nil cons cons 137 ref subst eqMp eqMp subst 1347 def subst 1271 ref refl 1295 ref nil 21 ref 1156 remove cons 1348 def 154 ref cons nil cons cons 1310 ref subst 1349 def appThm appThm trans appThm 1350 def nil 1225 remove 1276 ref nil cons cons 1339 remove cons nil cons cons 1351 def 1347 remove subst 1275 ref refl 1315 remove 1349 remove appThm appThm trans appThm sym 1048 ref refl nil 85 ref 28 ref 1046 ref appTerm 1048 ref appTerm 1352 def nil cons cons 86 ref 28 ref 1048 ref appTerm 1048 ref appTerm 1353 def nil cons cons nil cons cons nil cons cons 380 remove sym 1354 def nil 261 ref 73 ref 12 ref 370 remove 76 ref appTerm 1355 def appTerm 12 ref 366 remove 76 ref appTerm 1356 def appTerm 76 ref appTerm 1357 def appTerm 1358 def absTerm nil cons cons nil cons nil cons cons 934 remove subst 1359 def 73 ref nil 73 ref 1358 remove nil cons cons nil cons nil cons cons 80 ref subst 1360 def nil 42 ref 1355 ref nil cons 1361 def cons 43 ref 1357 remove nil cons 1362 def cons nil cons cons nil cons cons 1363 def 60 ref subst 1364 def 1363 remove 126 ref subst 1365 def nil 42 ref 1356 ref nil cons 1366 def cons 43 ref 263 ref cons nil cons 1367 def cons nil cons cons 1368 def 60 ref subst 1369 def 1368 remove 126 ref subst 1370 def nil 42 ref 721 remove cons 1367 ref cons nil cons cons 106 ref subst 1356 remove assume eqMp eqMp nil 85 ref 1366 remove cons 86 ref 263 remove cons nil cons cons nil cons cons 99 ref subst 1371 def deductAntisym eqMp eqMp nil 85 ref 1361 remove cons 86 ref 1362 remove cons nil cons cons nil cons cons 99 ref subst 1372 def deductAntisym eqMp eqMp absThm eqMp eqMp subst proveHyp nil 42 ref 288 ref 1352 remove appTerm 1353 remove appTerm nil cons cons 43 ref 28 ref 1061 ref 32 ref appTerm 1373 def appTerm 1374 def 1062 remove 32 ref appTerm 1375 def appTerm 1376 def nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 169 remove 1264 ref 155 ref appTerm 1377 def betaConv nil 1320 remove 43 ref 1377 remove nil cons cons nil cons cons nil cons cons 106 ref subst 108 ref 109 ref 1264 remove nil cons cons 167 ref cons nil cons cons 137 ref subst eqMp eqMp 1378 def subst eqMp 44 ref "_30380" 2 ref var 1379 def 28 ref 1271 ref 1379 remove varTerm appTerm appTerm 1275 remove 1375 ref appTerm 1380 def appTerm absTerm 1381 def 1373 ref appTerm 1382 def appTerm refl 1381 ref 1375 ref appTerm betaConv appThm 87 ref 1382 remove betaConv appThm 28 ref 1271 remove 1375 ref appTerm appTerm 1380 remove appTerm refl appThm trans 1381 remove refl 1376 remove assume appThm eqMp sym nil 21 ref 1274 ref nil cons cons 938 ref 1375 remove nil cons cons 152 ref 1270 ref nil cons cons nil cons 1383 def cons cons nil cons cons 21 ref 44 ref 28 ref 156 remove 939 ref appTerm 1384 def appTerm 150 remove 939 ref appTerm appTerm appTerm 214 remove appTerm absTerm 1385 def 32 ref appTerm 1386 def betaConv 152 ref 40 ref 1385 ref appTerm 1387 def absTerm 1388 def 155 ref appTerm 1389 def betaConv 938 ref 40 ref 1388 ref appTerm 1390 def absTerm 1391 def 939 ref appTerm 1392 def betaConv nil 40 ref 1391 ref appTerm 1393 def axiom nil 42 ref 1393 remove nil cons cons 43 ref 1392 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 1391 remove nil cons cons 985 ref cons nil cons cons 137 ref subst eqMp eqMp nil 42 ref 1390 remove nil cons cons 43 ref 1389 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 1388 remove nil cons cons 167 ref cons nil cons cons 137 ref subst eqMp eqMp nil 42 ref 1387 remove nil cons cons 43 ref 1386 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 1385 remove nil cons cons 112 ref cons nil cons cons 137 ref subst eqMp eqMp 1394 def subst sym "Number.Natural.<=" const 27 ref constTerm 1395 def refl 1396 def 143 ref appThm 185 remove appThm nil 1124 remove 1288 remove nil cons cons nil cons cons 21 ref 44 ref 1395 ref 1125 ref appTerm 1397 def 157 ref appTerm appTerm 1395 ref 155 ref appTerm 32 ref appTerm appTerm absTerm 1398 def 32 ref appTerm 1399 def betaConv 152 ref 40 ref 1398 ref appTerm 1400 def absTerm 1401 def 155 ref appTerm 1402 def betaConv nil 40 ref 1401 ref appTerm 1403 def axiom nil 42 ref 1403 remove nil cons cons 43 ref 1402 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 1401 remove nil cons cons 167 ref cons nil cons cons 137 ref subst eqMp eqMp nil 42 ref 1400 remove nil cons cons 43 ref 1399 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 1398 remove nil cons cons 112 ref cons nil cons cons 137 ref subst eqMp eqMp subst 1144 remove nil 73 ref 1395 ref 16 ref appTerm 32 ref appTerm 1404 def nil cons cons nil cons nil cons cons 80 ref subst 21 ref 1404 remove absTerm 1405 def 32 ref appTerm 1406 def betaConv nil 40 ref 1405 ref appTerm 1407 def axiom nil 42 ref 1407 remove nil cons cons 43 ref 1406 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 1405 remove nil cons cons 112 ref cons nil cons cons 137 ref subst eqMp eqMp eqMp subst trans trans sym 79 ref eqMp nil 42 ref 1395 ref 1045 ref appTerm 1408 def 1048 ref appTerm nil cons cons 43 ref 28 ref 149 ref 1269 ref appTerm 1409 def 1045 ref appTerm appTerm 1048 ref appTerm 1410 def nil cons 1411 def cons nil cons cons nil cons cons 106 ref subst proveHyp nil 1289 ref 152 ref 1338 ref cons nil cons 1412 def cons nil cons cons 152 ref 12 ref 1395 ref 32 ref appTerm 1413 def 155 ref appTerm 1414 def appTerm 28 ref 149 ref 1070 ref 155 ref appTerm 32 ref appTerm appTerm 32 ref appTerm appTerm 155 ref appTerm appTerm 1415 def absTerm 1416 def 155 ref appTerm 1417 def betaConv 21 ref 40 ref 1416 ref appTerm 1418 def absTerm 1419 def 32 ref appTerm 1420 def betaConv nil 40 ref 152 ref 40 ref 21 ref 1415 ref absTerm 1421 def appTerm 1422 def absTerm 1423 def appTerm 1424 def axiom nil 42 ref 1424 remove nil cons 1425 def cons 1426 def 43 ref 40 ref 1419 ref appTerm nil cons 1427 def cons nil cons cons nil cons cons 1428 def 106 ref subst proveHyp 1428 ref 60 ref subst 1428 remove 126 ref subst nil 109 ref 1419 remove nil cons cons 1429 def nil cons nil cons cons 207 ref subst 21 ref nil 73 ref 1418 remove nil cons 1430 def cons nil cons nil cons cons 80 ref subst nil 109 ref 1416 remove nil cons cons 1431 def nil cons nil cons cons 207 ref subst 152 ref nil 73 ref 1415 remove nil cons cons nil cons nil cons cons 80 ref subst 1421 ref 32 ref appTerm 1432 def betaConv 1423 ref 155 ref appTerm 1433 def betaConv nil 1426 remove 43 ref 1433 remove nil cons cons nil cons cons nil cons cons 106 ref subst 108 ref 109 ref 1423 remove nil cons cons 167 ref cons nil cons cons 137 ref subst eqMp eqMp nil 42 ref 1422 remove nil cons cons 43 ref 1432 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 1421 remove nil cons cons 112 ref cons nil cons cons 137 ref subst eqMp eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp nil 85 ref 1425 remove cons 86 ref 1427 ref cons nil cons cons nil cons cons 99 ref subst deductAntisym eqMp eqMp nil 42 ref 1427 remove cons 43 ref 1420 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 1429 remove 112 ref cons nil cons cons 137 ref subst eqMp eqMp nil 42 ref 1430 remove cons 43 ref 1417 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 1431 remove 167 ref cons nil cons cons 137 ref subst eqMp eqMp subst eqMp nil 85 ref 1411 remove cons 86 ref 28 ref 1409 remove 1047 ref appTerm appTerm 1048 ref appTerm 1434 def nil cons cons nil cons cons nil cons cons 1354 remove 1359 remove 73 ref 1360 remove 1364 remove 1365 remove 1369 remove 1370 remove nil 42 ref 88 remove nil cons cons 1367 remove cons nil cons cons 106 ref subst 1355 remove assume eqMp eqMp 1371 remove deductAntisym eqMp eqMp 1372 remove deductAntisym eqMp eqMp absThm eqMp eqMp subst proveHyp nil 42 ref 288 ref 1410 remove appTerm 1434 remove appTerm nil cons cons 43 ref 28 ref 1270 remove appTerm 1274 remove appTerm nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp nil 152 ref 1269 remove nil cons cons nil cons nil cons cons 1378 remove subst eqMp eqMp eqMp proveHyp eqMp eqMp eqMp nil 85 ref 1326 ref cons 86 ref 1321 ref cons nil cons 1435 def cons nil cons cons 99 ref subst deductAntisym eqMp nil 42 ref 1324 remove 65 ref appTerm 1436 def nil cons 1437 def cons 1322 remove cons nil cons cons 1438 def 60 ref subst 1438 remove 126 ref subst 1332 remove "_30376" 3 ref var 1439 def 28 ref 1067 ref 1439 remove varTerm appTerm 1048 ref appTerm 1440 def 1273 ref appTerm appTerm 1440 remove 1276 ref appTerm appTerm absTerm 65 ref appTerm betaConv appThm 1333 remove 28 ref 1067 ref 65 remove appTerm 1048 ref appTerm 1441 def 1273 ref appTerm appTerm 1441 remove 1276 remove appTerm appTerm refl appThm trans 1336 remove 1436 remove assume appThm eqMp sym 1084 ref 1340 remove 1241 ref subst appThm 1351 remove 1241 remove subst appThm nil 110 ref 1338 ref cons nil cons nil cons cons 1102 ref subst trans sym 79 ref eqMp eqMp eqMp nil 85 ref 1437 remove cons 1442 def 1435 ref cons nil cons cons 99 ref subst deductAntisym eqMp 357 remove 1266 ref appTerm 1443 def betaConv 360 remove nil 361 remove 43 ref 1443 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 260 ref 362 remove 262 remove 1266 ref nil cons 1444 def cons nil cons cons nil cons cons 137 ref subst eqMp eqMp nil 1442 remove 86 ref 1326 remove cons 365 ref 1321 remove cons nil cons cons cons nil cons cons 381 ref subst proveHyp proveHyp proveHyp eqMp nil 85 ref 1319 remove cons 1435 remove cons nil cons cons 99 ref subst deductAntisym eqMp eqMp nil 85 ref 1316 remove cons 86 ref 1317 remove cons nil cons cons nil cons cons 99 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp eqMp nil 42 ref 14 ref 1243 remove appTerm 1282 remove appTerm nil cons cons 43 ref 40 ref 21 ref 1258 remove absTerm 1445 def appTerm nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 13 ref 19 ref 1445 ref 16 ref appTerm betaConv appThm 19 ref 1445 ref 1045 ref appTerm betaConv appThm 144 ref 21 ref 13 ref 19 ref 1445 ref 32 ref appTerm betaConv 1446 def appThm 1445 ref 1046 ref appTerm betaConv appThm appThm 1445 ref 1048 ref appTerm betaConv appThm absThm appThm appThm appThm appThm 144 ref 21 ref 1446 remove absThm appThm appThm nil 8 remove 1445 remove nil cons cons nil cons nil cons cons 1049 ref 15 remove appTerm 1447 def betaConv 1044 remove nil 42 ref 1050 remove nil cons cons 43 ref 1447 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 196 remove 188 remove 1049 remove nil cons cons 1043 remove cons nil cons cons 137 ref subst eqMp eqMp subst eqMp eqMp eqMp eqMp absThm eqMp eqMp absThm eqMp nil 42 ref 1055 ref 1081 remove appTerm nil cons cons 43 ref 445 ref 1054 remove constTerm 1448 def 1053 ref 40 ref 21 ref 1374 ref 1076 remove appTerm absTerm appTerm absTerm appTerm nil cons 1449 def cons nil cons cons nil cons cons 106 ref subst proveHyp nil "h" 1 ref 30 ref 147 remove cons opType var 1074 remove nil cons cons nil cons nil cons cons 206 ref "h" 1 ref 1 ref 2 ref 429 ref cons opType 1450 def 1450 ref nil cons cons opType 1451 def var 1452 def 12 ref 0 ref 1 ref 1 ref 1450 ref 4 ref cons opType 4 ref cons opType 1453 def constTerm 1454 def "f" 1450 ref var 1455 def 1454 ref "g" 1450 remove var 1456 def 40 ref 21 ref 12 ref 40 ref 152 ref 1060 remove 275 ref 1455 ref varTerm 1457 def 155 ref appTerm appTerm 1456 ref varTerm 1458 def 155 ref appTerm appTerm 1459 def appTerm absTerm appTerm appTerm 275 ref 1452 ref varTerm 1460 def 1457 ref appTerm 32 ref appTerm 1461 def appTerm 1460 ref 1458 remove appTerm 32 ref appTerm appTerm 1462 def appTerm absTerm appTerm absTerm appTerm absTerm appTerm appTerm 445 ref 1453 remove constTerm 1455 ref 40 ref 21 ref 275 remove 1457 remove 32 ref appTerm appTerm 1461 remove appTerm absTerm appTerm absTerm appTerm 1463 def appTerm absTerm 1464 def 1460 ref appTerm 1465 def betaConv "s" 27 ref var 1466 def 14 ref 40 ref 110 ref 40 ref "y" 2 ref var 1467 def 12 ref 110 ref 1467 ref 288 ref 28 ref 149 ref 989 ref appTerm 1468 def 1045 ref appTerm 1469 def appTerm 1467 ref varTerm 1470 def appTerm 1471 def appTerm 28 ref 1468 remove 1047 remove appTerm 1472 def appTerm 1470 ref appTerm 1473 def appTerm 1474 def absTerm 1475 def absTerm 1476 def 989 ref appTerm 1477 def 1470 ref appTerm appTerm 1478 def 1466 remove varTerm 1479 def 989 ref appTerm 1470 ref appTerm appTerm absTerm appTerm absTerm appTerm appTerm "Relation.wellFounded" const 1480 def 1 ref 27 ref 4 ref cons opType 1481 def constTerm 1482 def 1479 remove appTerm appTerm absTerm 1483 def 209 ref appTerm betaConv sym 144 ref 110 ref 144 ref 1467 ref 13 ref 1477 remove betaConv 1470 ref refl 1484 def appThm 1475 remove 1470 ref appTerm betaConv trans appThm nil 21 ref 1470 ref nil cons cons 152 ref 989 ref nil cons cons nil cons 1485 def cons nil cons cons 21 ref 1167 remove 1397 remove 32 ref appTerm 1486 def appTerm 1487 def absTerm 1488 def 32 ref appTerm 1489 def betaConv 152 ref 40 ref 1488 ref appTerm 1490 def absTerm 1491 def 155 ref appTerm 1492 def betaConv 144 ref 152 ref 144 ref 21 ref 1487 remove assume sym 44 ref 1486 remove appTerm 211 ref appTerm 1493 def assume sym deductAntisym absThm appThm absThm appThm nil 40 ref 152 ref 40 ref 21 ref 1493 remove absTerm appTerm absTerm appTerm axiom eqMp nil 42 ref 40 ref 1491 ref appTerm nil cons cons 43 ref 1492 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 1491 remove nil cons cons 167 ref cons nil cons cons 137 ref subst eqMp eqMp nil 42 ref 1490 remove nil cons cons 43 ref 1489 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 1488 remove nil cons cons 112 ref cons nil cons cons 137 ref subst eqMp eqMp subst 1396 remove nil 1485 ref nil cons cons 152 ref 28 ref 1125 remove appTerm 1057 remove appTerm absTerm 1494 def 155 ref appTerm 1495 def betaConv nil 40 ref 1494 ref appTerm 1496 def axiom nil 42 ref 1496 remove nil cons cons 43 ref 1495 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 1494 remove nil cons cons 167 ref cons nil cons cons 137 ref subst eqMp eqMp 1497 def subst appThm 1484 remove appThm trans appThm absThm appThm absThm appThm sym nil 109 ref 110 ref 40 ref 1467 ref 12 ref 1474 ref appTerm 1395 ref 1469 ref appTerm 1498 def 1470 ref appTerm 1499 def appTerm 1500 def absTerm 1501 def appTerm 1502 def absTerm nil cons cons nil cons nil cons cons 207 ref subst 110 ref nil 73 ref 1502 remove nil cons cons nil cons nil cons cons 80 ref subst nil 109 ref 1501 remove nil cons cons nil cons nil cons cons 207 ref subst 1467 ref nil 73 ref 1500 remove nil cons cons nil cons nil cons cons 80 ref subst nil 42 ref 1474 remove nil cons 1503 def cons 43 ref 1499 remove nil cons 1504 def cons nil cons 1505 def cons nil cons cons 1506 def 60 ref subst 1506 remove 126 ref subst nil 42 ref 1473 ref nil cons 1507 def cons 1505 ref cons nil cons cons 1508 def 60 ref subst 1508 remove 126 ref subst 44 ref "_30374" 2 ref var 1509 def 1498 ref 1509 remove varTerm appTerm absTerm 1510 def 1470 ref appTerm 1511 def appTerm refl 1512 def 1510 ref 1472 ref appTerm betaConv appThm 87 ref 1511 remove betaConv appThm 1513 def 1498 ref 1472 remove appTerm refl appThm trans 1510 remove refl 1514 def 1473 remove assume sym appThm eqMp sym nil 1157 remove 1289 ref 1485 remove cons cons nil cons cons 938 ref 44 ref 1395 remove 158 ref appTerm 1384 remove appTerm appTerm 1413 ref 939 ref appTerm appTerm absTerm 1515 def 939 remove appTerm 1516 def betaConv 21 ref 40 ref 1515 ref appTerm 1517 def absTerm 1518 def 32 ref appTerm 1519 def betaConv 152 ref 40 ref 1518 ref appTerm 1520 def absTerm 1521 def 155 ref appTerm 1522 def betaConv nil 40 ref 1521 ref appTerm 1523 def axiom nil 42 ref 1523 remove nil cons cons 43 ref 1522 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 1521 remove nil cons cons 167 ref cons nil cons cons 137 ref subst eqMp eqMp nil 42 ref 1520 remove nil cons cons 43 ref 1519 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 1518 remove nil cons cons 112 ref cons nil cons cons 137 ref subst eqMp eqMp nil 42 ref 1517 remove nil cons cons 43 ref 1516 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 1515 remove nil cons cons 985 remove cons nil cons cons 137 ref subst eqMp eqMp subst 1408 remove refl 1084 ref 182 remove appThm 139 remove 143 remove appThm appThm nil 110 ref 34 remove 183 remove appTerm nil cons cons nil cons nil cons cons 1102 remove subst trans sym 79 ref eqMp 1524 def appThm 1291 ref nil 73 ref 1413 ref 157 remove appTerm 1525 def nil cons cons nil cons nil cons cons 80 ref subst 21 ref 1525 remove absTerm 1526 def 32 ref appTerm 1527 def betaConv nil 40 ref 1526 ref appTerm 1528 def axiom nil 42 ref 1528 remove nil cons cons 43 ref 1527 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 1526 remove nil cons cons 112 ref cons nil cons cons 137 ref subst eqMp eqMp eqMp subst trans trans sym 79 ref eqMp eqMp eqMp nil 85 ref 1507 ref cons 86 ref 1504 ref cons nil cons 1529 def cons nil cons cons 99 ref subst deductAntisym eqMp nil 42 ref 1471 ref nil cons 1530 def cons 1505 remove cons nil cons cons 1531 def 60 ref subst 1531 remove 126 ref subst 1512 remove "_30372" 2 remove var 1532 def 1498 ref 1532 remove varTerm appTerm absTerm 1469 ref appTerm betaConv appThm 1513 remove 1498 remove 1469 ref appTerm refl appThm trans 1514 remove 1471 remove assume sym appThm eqMp sym nil 21 ref 1469 remove nil cons cons nil cons nil cons cons 21 ref 1413 ref 32 ref appTerm absTerm 1533 def 32 ref appTerm 1534 def betaConv nil 40 ref 1533 ref appTerm 1535 def axiom nil 42 ref 1535 remove nil cons cons 43 ref 1534 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 1533 remove nil cons cons 112 ref cons nil cons cons 137 ref subst eqMp eqMp subst eqMp eqMp nil 85 ref 1530 remove cons 1536 def 1529 ref cons nil cons cons 99 ref subst deductAntisym eqMp nil 1536 remove 86 ref 1507 remove cons 365 remove 1504 remove cons nil cons cons cons nil cons cons 381 remove subst proveHyp proveHyp eqMp nil 85 ref 1503 remove cons 1529 remove cons nil cons cons 99 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp nil 42 ref 40 ref 110 remove 40 ref 1467 ref 1478 remove 209 ref 989 remove appTerm 1470 ref appTerm appTerm absTerm appTerm absTerm appTerm nil cons cons 43 ref 1482 ref 209 ref appTerm 1537 def nil cons cons nil cons cons nil cons cons 126 ref subst proveHyp nil 1537 remove axiom eqMp eqMp "A" 27 ref nil cons cons nil cons "P" 1481 ref var 1483 ref nil cons cons "x" 27 ref var 209 remove nil cons cons nil cons cons nil cons cons 936 ref subst proveHyp nil 42 ref 445 ref 1 ref 1481 remove 4 ref cons opType constTerm 1483 remove appTerm nil cons cons 43 ref 1482 remove 1476 ref appTerm nil cons 1538 def cons nil cons cons nil cons cons 106 ref subst proveHyp nil "r" 27 remove var 1476 ref nil cons cons nil cons nil cons cons 1539 def 206 remove "r" 274 ref var 1540 def 12 ref 445 ref 1 ref 1 ref 274 ref 4 ref cons opType 1541 def 4 ref cons opType 1542 def constTerm "s" 274 ref var 1543 def 14 ref 116 ref 121 ref 116 ref "y" 113 ref var 1544 def 12 ref 1540 ref varTerm 1545 def 122 ref appTerm 1544 remove varTerm 1546 def appTerm appTerm 1543 ref varTerm 1547 def 122 ref appTerm 1546 remove appTerm appTerm absTerm appTerm absTerm appTerm appTerm 1480 remove 1541 ref constTerm 1548 def 1547 ref appTerm 1549 def appTerm 1550 def absTerm 1551 def appTerm 1552 def appTerm 1553 def 1548 remove 1545 ref appTerm 1554 def appTerm 1555 def absTerm 1556 def 1545 ref appTerm 1557 def betaConv 0 ref 1542 remove constTerm 1558 def refl 1559 def 1540 ref 1559 remove 1543 ref 13 ref 19 remove 430 remove "B" 429 remove cons nil cons 1560 def cons 197 ref cons "s" 235 ref var 1561 def 44 ref "Relation.subrelation" const 1562 def 1 ref 235 ref 1 ref 235 ref 4 ref cons opType 1563 def nil cons cons opType constTerm "r" 235 ref var 1564 def varTerm 1565 def appTerm 1561 remove varTerm 1566 def appTerm appTerm 116 ref 121 ref 232 remove 233 remove 12 ref 1565 ref 122 ref appTerm 238 ref appTerm appTerm 1566 ref 122 ref appTerm 238 remove appTerm appTerm absTerm appTerm absTerm appTerm appTerm absTerm 1567 def 1566 ref appTerm 1568 def betaConv 1564 remove 0 ref 1 ref 1563 ref 4 ref cons opType constTerm 1569 def 1567 ref appTerm 1570 def absTerm 1571 def 1565 ref appTerm 1572 def betaConv nil 1569 remove 1571 ref appTerm 1573 def axiom nil 42 ref 1573 remove nil cons cons 43 ref 1572 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp "A" 235 ref nil cons cons nil cons 1574 def "P" 1563 remove var 1575 def 1571 remove nil cons cons "x" 235 remove var 1576 def 1565 remove nil cons cons nil cons cons nil cons cons 137 ref subst eqMp eqMp nil 42 ref 1570 remove nil cons cons 43 ref 1568 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 1574 remove 1575 remove 1567 remove nil cons cons 1576 remove 1566 remove nil cons cons nil cons cons nil cons cons 137 ref subst eqMp eqMp subst appThm 1549 ref refl appThm appThm 1554 ref refl appThm absThm appThm absThm appThm nil 1558 ref 1540 ref 1558 ref 1543 ref 12 ref 14 ref 1562 remove 1 ref 274 ref 1541 ref nil cons cons opType constTerm 1545 ref appTerm 1547 ref appTerm appTerm 1549 remove appTerm appTerm 1554 ref appTerm absTerm appTerm absTerm appTerm axiom eqMp nil 42 ref 1558 ref 1540 ref 1558 ref 1543 ref 12 ref 1550 ref appTerm 1554 ref appTerm absTerm 1577 def appTerm 1578 def absTerm 1579 def appTerm 1580 def nil cons 1581 def cons 1582 def 43 ref 1558 ref 1556 ref appTerm nil cons 1583 def cons nil cons cons nil cons cons 1584 def 106 ref subst proveHyp 1584 ref 60 ref subst 1584 remove 126 ref subst nil "P" 1541 remove var 1585 def 1556 remove nil cons cons 1586 def nil cons nil cons cons "A" 274 ref nil cons cons nil cons 1587 def 197 ref cons 198 remove subst 1588 def subst 1540 ref nil 73 ref 1555 remove nil cons cons nil cons nil cons cons 80 ref subst nil 42 ref 1552 remove nil cons 1589 def cons 1590 def 43 ref 1554 ref nil cons 1591 def cons nil cons 1592 def cons nil cons cons 1593 def 60 ref subst 1593 remove 126 ref subst nil 1582 ref 1592 ref cons nil cons cons 1594 def 106 ref subst nil 1590 remove 43 ref 12 ref 1580 remove appTerm 1554 ref appTerm 1595 def nil cons 1596 def cons nil cons 1597 def cons nil cons cons 106 ref subst nil 1585 ref 1543 ref 12 ref 1551 ref 1547 ref appTerm 1598 def appTerm 1595 ref appTerm 1599 def absTerm nil cons cons nil cons nil cons cons 1588 remove subst 1543 remove nil 73 ref 1599 remove nil cons cons nil cons nil cons cons 80 ref subst nil 42 ref 1598 ref nil cons 1600 def cons 1597 ref cons nil cons cons 1601 def 60 ref subst 1601 remove 126 ref subst 1598 ref betaConv 1598 remove assume eqMp nil 42 ref 1550 remove nil cons 1602 def cons 1603 def 1597 remove cons nil cons cons 1604 def 106 ref subst proveHyp 1604 ref 60 ref subst 1604 remove 126 ref subst 1594 ref 60 ref subst 1594 remove 126 ref subst nil 1603 remove 1592 remove cons nil cons cons 106 ref subst 1577 ref 1547 ref appTerm 1605 def betaConv 1579 ref 1545 ref appTerm 1606 def betaConv nil 1582 remove 43 ref 1606 remove nil cons cons nil cons cons nil cons cons 106 ref subst 1587 ref 1585 ref 1579 remove nil cons cons "x" 274 remove var 1607 def 1545 ref nil cons cons nil cons 1608 def cons nil cons cons 137 ref subst eqMp eqMp nil 42 ref 1578 remove nil cons cons 43 ref 1605 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 1587 ref 1585 ref 1577 remove nil cons cons 1607 ref 1547 remove nil cons cons nil cons cons nil cons cons 137 ref subst eqMp eqMp eqMp eqMp nil 85 ref 1581 remove cons 1609 def 86 ref 1591 remove cons nil cons 1610 def cons nil cons cons 99 ref subst deductAntisym eqMp eqMp nil 85 ref 1602 remove cons 86 ref 1596 remove cons nil cons 1611 def cons nil cons cons 99 ref subst deductAntisym eqMp eqMp eqMp nil 85 ref 1600 remove cons 1611 ref cons nil cons cons 99 ref subst deductAntisym eqMp eqMp absThm eqMp nil 42 ref 1558 ref 1607 ref 12 ref 1551 ref 1607 remove varTerm appTerm appTerm 1595 ref appTerm absTerm appTerm nil cons cons 43 ref 1553 remove 1595 remove appTerm nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 1587 ref 1585 ref 1551 remove nil cons cons 1611 remove cons nil cons cons 739 ref subst eqMp eqMp eqMp eqMp nil 85 ref 1589 remove cons 1610 remove cons nil cons cons 99 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp nil 1609 remove 86 ref 1583 ref cons nil cons cons nil cons cons 99 ref subst deductAntisym eqMp eqMp nil 42 ref 1583 remove cons 43 ref 1557 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 1587 ref 1586 remove 1608 ref cons nil cons cons 137 ref subst eqMp eqMp subst subst eqMp nil 42 ref 1538 remove cons 43 ref 0 ref 1 ref 1 ref 1451 ref 4 ref cons opType 1612 def 4 ref cons opType constTerm 1613 def 1452 ref 12 ref 1454 ref 1455 ref 1454 ref 1456 ref 40 ref 21 ref 12 ref 40 ref 152 ref 12 ref 1476 remove 155 ref appTerm 1614 def 32 ref appTerm appTerm 1459 ref appTerm absTerm appTerm appTerm 1462 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm appTerm 1463 ref appTerm absTerm appTerm 1615 def nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 1539 remove 107 remove 1560 remove cons 197 remove cons 1540 remove 12 ref 1554 remove appTerm 0 remove 1 ref 1 ref 1 ref 431 ref 443 remove cons opType 1616 def 4 ref cons opType 4 remove cons opType constTerm "h" 1616 remove var 1617 def 12 ref 441 ref "f" 431 ref var 1618 def 441 remove "g" 431 remove var 1619 def 116 ref 121 ref 12 ref 116 ref "z" 113 remove var 1620 def 12 ref 1545 ref 1620 remove varTerm 1621 def appTerm 122 ref appTerm appTerm 25 remove 1 remove 229 remove 234 remove cons opType constTerm 1622 def 1618 ref varTerm 1623 def 1621 ref appTerm appTerm 1619 remove varTerm 1624 def 1621 remove appTerm appTerm appTerm absTerm appTerm appTerm 1622 ref 1617 remove varTerm 1625 def 1623 ref appTerm 122 ref appTerm 1626 def appTerm 1625 remove 1624 remove appTerm 122 ref appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm appTerm 445 remove 440 remove constTerm 1618 remove 116 remove 121 remove 1622 remove 1623 remove 122 remove appTerm appTerm 1626 remove appTerm absTerm appTerm absTerm appTerm appTerm absTerm appTerm appTerm absTerm 1627 def 1545 remove appTerm 1628 def betaConv nil 1558 remove 1627 ref appTerm 1629 def axiom nil 42 ref 1629 remove nil cons cons 43 ref 1628 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 1587 remove 1585 remove 1627 remove nil cons cons 1608 remove cons nil cons cons 137 ref subst eqMp eqMp subst subst eqMp 1613 ref refl 1452 remove 13 ref 1454 remove refl 1630 def 1455 remove 1630 remove 1456 remove 144 ref 21 ref 13 ref 144 ref 152 ref 13 ref 1614 remove betaConv 223 remove appThm 1467 remove 288 remove 1058 remove 1470 ref appTerm appTerm 1059 remove 1470 remove appTerm appTerm absTerm 32 ref appTerm betaConv trans appThm 1459 remove refl appThm absThm appThm appThm 1462 remove refl appThm absThm appThm absThm appThm absThm appThm appThm 1463 remove refl appThm absThm appThm 1615 remove assume eqMp proveHyp 1631 def nil 42 ref 1613 remove 1464 ref appTerm 1632 def nil cons cons 43 ref 1465 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp "A" 1451 ref nil cons cons nil cons "P" 1612 remove var 1464 remove nil cons cons "x" 1451 remove var 1460 remove nil cons cons nil cons cons nil cons cons 137 ref subst eqMp eqMp subst subst eqMp nil 42 ref 1449 remove cons 43 ref 1448 ref 1053 ref 14 ref 28 ref 1312 remove appTerm 16 remove appTerm 1633 def appTerm 14 remove 28 ref 1061 ref 1045 ref appTerm appTerm 1045 remove appTerm 1634 def appTerm 40 ref 21 ref 28 ref 1061 ref 1048 ref appTerm appTerm 149 remove 1061 ref 1046 ref appTerm 1635 def appTerm 1373 ref appTerm 1636 def appTerm 1637 def absTerm 1638 def appTerm 1639 def appTerm 1640 def appTerm absTerm 1641 def appTerm 1642 def nil cons 1643 def cons nil cons 1644 def cons nil cons cons 106 ref subst 13 remove 1448 ref refl 1053 ref 144 remove 21 ref 1374 ref refl 1085 remove appThm absThm appThm absThm appThm appThm 1642 ref refl appThm sym nil 1052 ref 1053 ref 12 ref 1053 ref 40 ref 21 ref 1374 remove 1257 remove appTerm absTerm 1645 def appTerm 1646 def absTerm 1647 def 1061 ref appTerm 1648 def appTerm 1642 ref appTerm 1649 def absTerm nil cons cons nil cons nil cons cons 1083 remove subst 1053 remove nil 73 ref 1649 remove nil cons cons nil cons nil cons cons 80 ref subst nil 42 ref 1648 ref nil cons 1650 def cons 1644 ref cons nil cons cons 1651 def 60 ref subst 1651 remove 126 ref subst 1648 ref betaConv 1648 remove assume eqMp nil 42 ref 1646 remove nil cons 1652 def cons 1653 def 1644 remove cons nil cons cons 1654 def 106 ref subst proveHyp 1654 ref 60 remove subst 1654 remove 126 ref subst 1641 ref 1061 ref appTerm betaConv sym 1084 ref 24 remove 1645 ref 32 ref appTerm 1655 def betaConv nil 1653 remove 43 ref 1655 remove nil cons cons nil cons cons nil cons cons 106 ref subst 108 ref 109 ref 1645 remove nil cons cons 112 ref cons nil cons cons 137 ref subst eqMp eqMp 1656 def subst appThm 1223 remove appThm sym 1242 remove eqMp nil 42 ref 1633 remove nil cons cons 43 ref 1640 remove nil cons cons nil cons cons nil cons cons 126 ref subst proveHyp 1084 ref 1291 remove 1656 ref subst appThm 1292 ref appThm sym 1314 remove eqMp nil 42 ref 1634 remove nil cons cons 43 ref 1639 remove nil cons cons nil cons cons nil cons cons 126 remove subst proveHyp nil 109 ref 1638 remove nil cons cons nil cons nil cons cons 207 remove subst 21 ref nil 73 ref 1637 remove nil cons cons nil cons nil cons cons 80 ref subst 1084 ref nil 21 ref 1338 remove cons nil cons nil cons cons 1656 remove subst appThm 1636 ref refl 1657 def appThm sym nil 73 ref 1444 remove cons nil cons nil cons cons 73 ref 44 ref 356 remove appTerm 255 remove appTerm absTerm 1658 def 76 remove appTerm 1659 def betaConv nil 258 remove 1658 ref appTerm 1660 def axiom nil 42 ref 1660 remove nil cons cons 43 ref 1659 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 260 remove 261 remove 1658 remove nil cons cons 264 remove cons nil cons cons 137 ref subst eqMp eqMp subst nil 1348 ref 1412 remove cons nil cons cons 21 ref 44 ref 250 remove 211 remove appTerm appTerm 1414 remove appTerm absTerm 1661 def 32 ref appTerm 1662 def betaConv 152 ref 40 ref 1661 ref appTerm 1663 def absTerm 1664 def 155 ref appTerm 1665 def betaConv nil 40 ref 1664 ref appTerm 1666 def axiom nil 42 ref 1666 remove nil cons cons 43 ref 1665 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 1664 remove nil cons cons 167 ref cons nil cons cons 137 ref subst eqMp eqMp nil 42 ref 1663 remove nil cons cons 43 ref 1662 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 1661 remove nil cons cons 112 ref cons nil cons cons 137 ref subst eqMp eqMp subst nil 153 remove 1348 remove nil cons cons nil cons cons nil 73 remove 1413 remove 158 remove appTerm 1667 def nil cons cons nil cons nil cons cons 80 remove subst 21 ref 1667 remove absTerm 1668 def 32 remove appTerm 1669 def betaConv 152 ref 40 ref 1668 ref appTerm 1670 def absTerm 1671 def 155 remove appTerm 1672 def betaConv nil 40 remove 1671 ref appTerm 1673 def axiom nil 42 ref 1673 remove nil cons cons 43 ref 1672 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 ref 109 ref 1671 remove nil cons cons 167 remove cons nil cons cons 137 ref subst eqMp eqMp nil 42 ref 1670 remove nil cons cons 43 ref 1669 remove nil cons cons nil cons cons nil cons cons 106 ref subst proveHyp 108 remove 109 remove 1668 remove nil cons cons 112 remove cons nil cons cons 137 remove subst eqMp eqMp eqMp subst trans trans sym 79 remove eqMp 44 remove "_30382" 3 remove var 1674 def 28 remove 1067 remove 1674 remove varTerm appTerm 1048 remove appTerm 1273 remove appTerm appTerm 1636 ref appTerm absTerm 1675 def 1266 remove appTerm 1676 def appTerm refl 1675 ref 254 remove appTerm betaConv appThm 87 remove 1676 remove betaConv appThm 1335 remove 1636 remove appTerm refl appThm trans 1675 remove refl 1337 remove appThm eqMp sym 1350 remove 1657 remove appThm nil 21 remove 1635 ref nil cons cons 938 remove 1373 remove nil cons cons 1383 remove cons cons nil cons cons 1394 remove subst trans sym 1084 remove 1295 ref 1070 remove refl 1677 def 151 remove 1524 remove appThm nil 1289 ref 154 remove cons nil cons cons 168 remove subst trans appThm 1292 ref appThm appThm appThm 1635 remove refl appThm sym 1295 remove 1677 remove nil 152 remove 1046 remove nil cons cons nil cons 1678 def nil cons cons 1497 remove subst appThm 1292 remove appThm nil 1289 remove 1678 remove cons nil cons cons 1310 remove subst trans appThm eqMp eqMp eqMp proveHyp eqMp eqMp absThm eqMp eqMp eqMp eqMp 1082 ref 1052 ref 1641 remove nil cons cons "x" 30 remove var 1679 def 1061 remove nil cons cons nil cons cons nil cons cons 936 remove subst proveHyp eqMp nil 85 ref 1652 remove cons 86 remove 1643 remove cons nil cons 1680 def cons nil cons cons 99 ref subst deductAntisym eqMp eqMp eqMp nil 85 remove 1650 remove cons 1680 ref cons nil cons cons 99 remove subst deductAntisym eqMp eqMp absThm eqMp nil 42 remove 1055 remove 1679 ref 12 ref 1647 ref 1679 remove varTerm appTerm appTerm 1642 ref appTerm absTerm appTerm nil cons cons 43 remove 12 remove 1448 remove 1647 ref appTerm appTerm 1642 ref appTerm nil cons cons nil cons cons nil cons cons 106 remove subst proveHyp 1082 remove 1052 remove 1647 remove nil cons cons 1680 remove cons nil cons cons 739 remove subst eqMp eqMp eqMp proveHyp nil 1642 remove thm 1631 remove nil 1632 remove thm