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