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