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