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