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