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