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