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