path: "vendor/opentheory/data/theories/natural-fibonacci-def/natural-fibonacci-def.art"
6 version "Data.Bool./\\" const "->" typeOp 0 def "bool" typeOp nil opType 1 def 0 ref 1 ref 1 ref nil cons 2 def cons opType 3 def nil cons 4 def cons opType 5 def constTerm 6 def refl 7 def nil "t" 1 ref var 8 def "Number.Natural.Fibonacci.zeckendorf" "zeckendorf" 0 ref "Data.List.list" typeOp 9 def 2 ref opType 10 def 2 ref cons opType 11 def var 12 def nil cons cons nil cons 12 ref 6 ref "=" const 13 def 5 ref constTerm 14 def 12 remove varTerm 15 def "Data.List.[]" const 16 def 10 ref constTerm 17 def appTerm appTerm "Data.Bool.T" const 1 ref constTerm 18 def appTerm appTerm "Data.Bool.!" const 19 def 0 ref 3 ref 2 ref cons opType 20 def constTerm 21 def "h" 1 ref var 22 def 19 ref 0 ref 11 ref 2 ref cons opType 23 def constTerm 24 def "t" 10 ref var 25 def 14 ref 15 ref "Data.List.::" const 26 def 0 ref 1 ref 0 ref 10 ref 10 ref nil cons 27 def cons opType nil cons 28 def cons opType constTerm 29 def 22 ref varTerm 30 def appTerm 25 ref varTerm 31 def appTerm 32 def appTerm appTerm "Data.Bool.cond" const 33 def 0 ref 1 ref 5 ref nil cons cons opType constTerm "Data.List.null" const 11 ref constTerm 31 ref appTerm appTerm 30 ref appTerm 34 def 6 ref "Data.Bool.~" const 3 ref constTerm 35 def 6 ref 30 ref appTerm "Data.List.head" const 11 ref constTerm 31 ref appTerm appTerm appTerm appTerm 36 def 15 ref 31 ref appTerm appTerm appTerm appTerm absTerm appTerm absTerm appTerm appTerm absTerm 37 def refl 38 def 13 ref 0 ref 11 ref 23 ref nil cons cons opType constTerm 15 ref appTerm "select" const 39 def 0 ref 23 ref 11 ref nil cons 40 def cons opType constTerm 41 def 37 ref appTerm appTerm assume sym appThm 37 ref 15 remove appTerm betaConv trans "A" 40 ref cons nil cons nil nil cons 42 def cons nil 13 ref 0 ref 0 ref 0 ref "A" varType 43 def 2 ref cons opType 44 def 2 ref cons opType 45 def 0 ref 45 ref 2 ref cons opType 46 def nil cons cons opType constTerm 47 def "Data.Bool.?" const 48 def 45 ref constTerm 49 def appTerm 50 def "p" 44 ref var 51 def 51 ref varTerm 52 def 39 ref 0 ref 44 ref 43 ref nil cons 53 def cons opType constTerm 52 ref appTerm appTerm 54 def absTerm appTerm axiom 55 def subst 38 remove appThm "p" 23 ref var 56 def 56 remove varTerm 57 def 41 remove 57 remove appTerm appTerm absTerm 37 remove appTerm betaConv trans 48 ref 0 ref 23 remove 2 ref cons opType constTerm refl "fn" 11 ref var 58 def 6 ref 14 ref 58 remove varTerm 59 def 17 ref appTerm appTerm 18 ref appTerm appTerm refl 21 ref refl 60 def 22 ref 24 ref refl 61 def 25 ref 14 ref 59 ref 32 ref appTerm appTerm refl 22 ref 25 ref "_31859" 1 ref var 62 def 34 ref 36 ref 62 remove varTerm appTerm appTerm absTerm 63 def absTerm 64 def absTerm 65 def 30 ref appTerm betaConv 31 ref refl 66 def appThm 64 remove 31 ref appTerm betaConv trans 59 remove 31 ref appTerm 67 def refl appThm 63 remove 67 remove appTerm betaConv trans appThm absThm appThm absThm appThm appThm absThm appThm nil "f" 0 ref 1 ref 0 ref 10 ref 4 remove cons opType nil cons cons opType var 65 remove nil cons cons "b" 1 ref var 68 def 18 ref nil cons 69 def cons nil cons cons nil cons cons "A" 2 ref cons 70 def "B" 2 ref cons nil cons 71 def cons 42 ref cons "f" 0 ref 43 ref 0 ref 9 remove 53 ref opType 72 def 0 ref "B" varType 73 def 73 ref nil cons 74 def cons opType nil cons 75 def cons opType nil cons cons opType 76 def var 77 def 48 ref 0 ref 0 ref 0 ref 72 ref 74 ref cons opType 78 def 2 ref cons opType 2 ref cons opType constTerm "fn" 78 remove var 79 def 6 ref 13 ref 0 ref 73 ref 0 ref 73 ref 2 ref cons opType 80 def nil cons 81 def cons opType constTerm 82 def 79 remove varTerm 83 def 16 remove 72 ref constTerm appTerm appTerm "b" 73 ref var 84 def varTerm 85 def appTerm appTerm 19 ref 45 ref constTerm 86 def "h" 43 ref var 87 def 19 ref 0 ref 0 ref 72 ref 2 ref cons opType 88 def 2 ref cons opType constTerm "t" 72 ref var 89 def 82 ref 83 ref 26 remove 0 ref 43 ref 0 ref 72 ref 72 ref nil cons 90 def cons opType nil cons cons opType constTerm 87 remove varTerm 91 def appTerm 89 remove varTerm 92 def appTerm appTerm appTerm 77 remove varTerm 93 def 91 remove appTerm 92 ref appTerm 83 remove 92 remove appTerm appTerm appTerm absTerm appTerm absTerm appTerm appTerm absTerm appTerm absTerm 94 def 93 ref appTerm 95 def betaConv 84 ref 19 ref 0 ref 0 ref 76 ref 2 ref cons opType 96 def 2 ref cons opType constTerm 94 ref appTerm 97 def absTerm 98 def 85 ref appTerm 99 def betaConv nil 19 ref 0 ref 80 ref 2 ref cons opType 100 def constTerm 101 def 98 ref appTerm 102 def axiom nil "p" 1 ref var 103 def 102 remove nil cons cons "q" 1 ref var 104 def 99 remove nil cons cons nil cons cons nil cons cons 14 ref "Data.Bool.==>" const 5 ref constTerm 105 def 103 ref varTerm 106 def appTerm 107 def 104 ref varTerm 108 def appTerm 109 def appTerm 110 def refl 103 ref 104 ref 14 ref 6 ref 106 ref appTerm 111 def 108 ref appTerm 112 def appTerm 113 def 106 ref appTerm absTerm 114 def absTerm 115 def 106 ref appTerm betaConv 108 ref refl 116 def appThm 114 remove 108 ref appTerm betaConv trans appThm nil 13 ref 0 ref 5 ref 0 ref 5 ref 2 ref cons opType 117 def nil cons cons opType constTerm 118 def 105 ref appTerm 115 remove appTerm axiom 106 ref refl 119 def appThm 116 ref appThm eqMp 120 def sym 121 def 113 remove refl 104 ref 13 ref 0 ref 117 ref 0 ref 117 remove 2 ref cons opType nil cons cons opType constTerm 122 def "f" 5 ref var 123 def 123 ref varTerm 124 def 106 ref appTerm 108 ref appTerm absTerm 125 def appTerm 123 ref 124 ref 18 ref appTerm 18 ref appTerm absTerm 126 def appTerm absTerm 127 def 108 ref appTerm betaConv appThm 13 ref 0 ref 3 ref 20 remove nil cons cons opType constTerm 128 def 111 remove appTerm refl 103 ref 127 remove absTerm 129 def 106 ref appTerm betaConv appThm nil 118 ref 6 ref appTerm 129 ref appTerm axiom 130 def 119 remove appThm eqMp 116 ref appThm eqMp 131 def sym 123 ref 124 ref refl nil 8 ref 106 ref nil cons 132 def cons nil cons nil cons cons 14 ref 8 ref varTerm 133 def appTerm 134 def 18 ref appTerm 135 def assume sym nil 18 ref axiom 136 def eqMp 133 ref assume 136 ref deductAntisym deductAntisym 137 def subst 106 ref assume 138 def eqMp appThm nil 8 ref 108 ref nil cons 139 def cons nil cons nil cons cons 137 ref subst 108 ref assume 140 def eqMp appThm absThm eqMp 141 def nil "P" 1 ref var 142 def 132 ref cons "Q" 1 ref var 143 def 139 ref cons nil cons 144 def cons nil cons cons 14 ref refl 145 def 123 ref 124 remove 142 ref varTerm 146 def appTerm 147 def 143 ref varTerm 148 def appTerm absTerm 149 def 103 ref 104 ref 106 ref absTerm absTerm 150 def appTerm betaConv 150 ref 146 ref appTerm betaConv 148 ref refl 151 def appThm 104 ref 146 ref absTerm 148 ref appTerm betaConv trans trans appThm 126 ref 150 ref appTerm betaConv 150 ref 18 ref appTerm betaConv 18 ref refl 152 def appThm 104 ref 18 ref absTerm 18 ref appTerm betaConv trans trans appThm 14 ref 6 ref 146 ref appTerm 153 def 148 ref appTerm 154 def appTerm refl 104 ref 122 remove 123 remove 147 remove 108 ref appTerm absTerm appTerm 126 ref appTerm absTerm 148 ref appTerm betaConv appThm 128 ref 153 remove appTerm refl 129 remove 146 ref appTerm betaConv appThm 130 remove 146 ref refl 155 def appThm eqMp 151 ref appThm eqMp 154 remove assume eqMp 156 def 150 remove refl appThm eqMp sym 136 ref eqMp 157 def subst 158 def deductAntisym eqMp 120 remove 109 ref assume eqMp sym 138 ref eqMp 145 ref 125 remove 103 ref 104 ref 108 ref absTerm 159 def absTerm 160 def appTerm betaConv 160 ref 106 ref appTerm betaConv 116 remove appThm 159 ref 108 ref appTerm betaConv trans trans appThm 126 remove 160 ref appTerm betaConv 160 ref 18 ref appTerm betaConv 152 remove appThm 159 ref 18 ref appTerm betaConv trans trans 161 def appThm 131 remove 112 remove assume eqMp 160 ref refl 162 def appThm eqMp sym 136 ref eqMp 163 def proveHyp 164 def deductAntisym 165 def subst proveHyp "A" 74 ref cons nil cons 166 def "P" 80 remove var 167 def 98 remove nil cons cons "x" 73 ref var 85 ref nil cons cons nil cons 168 def cons nil cons cons nil 103 ref 86 ref "P" 44 ref var 169 def varTerm 170 def appTerm 171 def nil cons 172 def cons 104 ref 170 ref "x" 43 ref var 173 def varTerm 174 def appTerm 175 def nil cons 176 def cons nil cons cons nil cons cons 177 def 121 ref subst 177 remove 163 remove 141 remove deductAntisym 178 def subst 14 ref 175 ref appTerm refl 173 ref 18 ref absTerm 179 def 174 ref appTerm betaConv appThm 51 ref 13 ref 0 ref 44 ref 45 ref nil cons cons opType constTerm 52 ref appTerm 179 remove appTerm absTerm 180 def 170 ref appTerm betaConv 181 def nil 47 remove 86 ref appTerm 180 remove appTerm axiom 170 ref refl 182 def appThm 183 def 171 ref assume eqMp eqMp 174 ref refl 184 def appThm eqMp sym 136 ref eqMp eqMp nil 142 ref 172 remove cons 143 ref 176 ref cons nil cons cons nil cons cons 157 ref subst deductAntisym eqMp 185 def subst eqMp eqMp nil 103 ref 97 remove nil cons cons 104 ref 95 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp "A" 76 ref nil cons cons nil cons "P" 96 remove var 94 remove nil cons cons "x" 76 remove var 93 remove nil cons cons nil cons cons nil cons cons 185 ref subst eqMp eqMp 186 def subst subst eqMp eqMp eqMp defineConstList 187 def pop hdTl pop 11 ref constTerm 188 def 17 ref appTerm 189 def nil cons 190 def cons nil cons nil cons cons 8 ref 14 ref 135 ref appTerm 133 ref appTerm absTerm 191 def 133 ref appTerm 192 def betaConv nil 21 ref 191 ref appTerm 193 def axiom nil 103 ref 193 remove nil cons cons 104 ref 192 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 70 ref nil cons 194 def "P" 3 remove var 195 def 191 remove nil cons cons "x" 1 ref var 196 def 133 ref nil cons cons nil cons 197 def cons nil cons cons 185 ref subst eqMp eqMp subst appThm 21 ref 22 ref 24 ref 25 ref 14 ref 188 ref 32 ref appTerm appTerm 34 remove 36 remove 188 remove 31 ref appTerm appTerm appTerm appTerm absTerm appTerm absTerm appTerm 198 def refl appThm 187 remove eqMp 199 def nil 142 ref 190 remove cons 143 ref 198 ref nil cons cons nil cons cons nil cons cons 200 def 157 ref subst proveHyp nil 189 remove thm "Number.Natural.Fibonacci.all" "Data.Stream.fromFunction" const 0 ref 0 ref "Number.Natural.natural" typeOp nil opType 201 def 201 ref nil cons 202 def cons 203 def opType 204 def "Data.Stream.stream" typeOp 202 ref opType 205 def nil cons cons opType constTerm "Number.Natural.fibonacci" "f" 204 ref var 206 def nil cons cons nil cons 206 ref 6 ref 13 ref 0 ref 201 ref 0 ref 201 ref 2 ref cons opType 207 def nil cons cons opType 208 def constTerm 209 def 206 remove varTerm 210 def "Number.Natural.zero" const 201 ref constTerm 211 def appTerm appTerm 211 ref appTerm appTerm 6 ref 209 ref 210 ref "Number.Natural.bit1" const 204 ref constTerm 211 ref appTerm 212 def appTerm appTerm 212 ref appTerm appTerm 19 ref 0 ref 207 ref 2 ref cons opType 213 def constTerm 214 def "n" 201 ref var 215 def 209 ref 210 ref "Number.Natural.+" const 0 ref 201 ref 204 ref nil cons 216 def cons opType 217 def constTerm 218 def 215 ref varTerm 219 def appTerm 220 def "Number.Natural.bit0" const 204 ref constTerm 212 ref appTerm appTerm 221 def appTerm appTerm 218 ref 210 ref 220 remove 212 ref appTerm 222 def appTerm appTerm 210 ref 219 ref appTerm appTerm appTerm absTerm appTerm appTerm appTerm absTerm 223 def refl 224 def 13 ref 0 ref 204 ref 0 ref 204 ref 2 ref cons opType 225 def nil cons cons opType constTerm 226 def 210 ref appTerm 39 ref 0 ref 225 ref 216 ref cons opType constTerm 227 def 223 ref appTerm appTerm assume sym appThm 223 ref 210 remove appTerm betaConv trans "A" 216 remove cons nil cons 42 ref cons 55 ref subst 224 remove appThm "p" 225 ref var 228 def 228 remove varTerm 229 def 227 remove 229 remove appTerm appTerm absTerm 223 ref appTerm betaConv trans nil 48 ref 0 ref 225 remove 2 ref cons opType constTerm 223 remove appTerm axiom eqMp eqMp defineConstList 230 def pop hdTl pop 204 remove constTerm 231 def appTerm 232 def defineConst 233 def pop 234 def pop 233 remove nil 13 ref 0 ref 205 ref 0 ref 205 ref 2 ref cons opType nil cons cons opType constTerm 234 remove 205 remove constTerm appTerm 232 remove appTerm thm 230 ref nil 142 ref 209 ref 231 ref 211 ref appTerm appTerm 211 ref appTerm 235 def nil cons cons 143 ref 6 ref 209 ref 231 ref 212 ref appTerm appTerm 212 ref appTerm 236 def appTerm 214 ref 215 ref 209 ref 231 ref 221 remove appTerm appTerm 218 ref 231 ref 222 remove appTerm appTerm 231 remove 219 ref appTerm appTerm appTerm absTerm appTerm 237 def appTerm nil cons cons nil cons cons nil cons cons 238 def 157 ref subst proveHyp nil 235 remove thm 230 remove 238 remove 145 ref 149 remove 160 ref appTerm betaConv 160 remove 146 ref appTerm betaConv 151 ref appThm 159 remove 148 ref appTerm betaConv trans trans appThm 161 remove appThm 156 remove 162 remove appThm eqMp sym 136 ref eqMp 239 def subst proveHyp 240 def nil 142 ref 236 ref nil cons cons 143 ref 237 ref nil cons cons nil cons cons nil cons cons 241 def 157 ref subst proveHyp nil 236 remove thm "Number.Natural.Fibonacci.decode.dest" "decode_fib_dest" 0 ref 201 ref 0 ref 201 ref 0 ref 10 ref 202 ref cons opType 242 def nil cons cons opType nil cons cons opType 243 def var 244 def nil cons cons nil cons 244 ref 6 ref 214 ref "f" 201 ref var 245 def 214 ref "p" 201 ref var 246 def 209 ref 244 ref varTerm 247 def 245 ref varTerm 248 def appTerm 246 ref varTerm 249 def appTerm 250 def 17 ref appTerm appTerm 211 ref appTerm absTerm appTerm absTerm appTerm appTerm 214 ref 245 ref 214 ref 246 ref 21 ref 22 ref 24 ref 25 ref 209 ref 250 remove 32 ref appTerm appTerm "s" 201 ref var 251 def 215 ref 33 ref 0 ref 1 ref 217 ref nil cons 252 def cons opType constTerm 253 def 30 ref appTerm 218 ref 251 ref varTerm 254 def appTerm 255 def 219 ref appTerm 256 def appTerm 219 ref appTerm absTerm 257 def 247 ref 254 ref appTerm 248 ref appTerm 31 ref appTerm appTerm absTerm 218 ref 248 ref appTerm 258 def 249 ref appTerm 259 def appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm appTerm absTerm 260 def refl 261 def 13 ref 0 ref 243 ref 0 ref 243 ref 2 ref cons opType 262 def nil cons cons opType constTerm 263 def 247 ref appTerm 264 def 39 ref 0 ref 262 ref 243 ref nil cons 265 def cons opType constTerm 266 def 260 ref appTerm appTerm assume sym appThm 260 ref 247 ref appTerm betaConv 267 def trans "A" 265 remove cons nil cons 268 def 42 ref cons 55 ref subst 261 remove appThm "p" 262 ref var 269 def 269 remove varTerm 270 def 266 remove 270 remove appTerm appTerm absTerm 260 ref appTerm betaConv trans 48 ref 0 ref 0 ref 0 ref 10 ref 252 ref cons opType 271 def 2 ref cons opType 272 def 2 ref cons opType 273 def constTerm 274 def refl "fn" 271 ref var 275 def 6 ref 13 ref 0 ref 217 ref 0 ref 217 ref 2 ref cons opType nil cons cons opType constTerm 276 def 275 remove varTerm 277 def 17 ref appTerm appTerm 245 ref 246 ref 211 ref absTerm 278 def absTerm 279 def appTerm appTerm refl 60 ref 22 ref 61 ref 25 ref 276 ref 277 ref 32 ref appTerm appTerm refl 22 ref 25 ref "_31712" 217 ref var 280 def 245 ref 246 ref 251 ref 257 ref 280 remove varTerm 254 ref appTerm 248 ref appTerm appTerm absTerm 259 ref appTerm absTerm absTerm absTerm 281 def absTerm 282 def absTerm 283 def 30 ref appTerm betaConv 66 ref appThm 282 remove 31 ref appTerm betaConv trans 277 remove 31 ref appTerm 284 def refl appThm 281 remove 284 remove appTerm betaConv trans appThm absThm appThm absThm appThm appThm absThm appThm nil "f" 0 ref 1 ref 0 ref 10 ref 0 ref 217 ref 252 ref cons opType nil cons cons opType nil cons cons opType var 283 remove nil cons cons "b" 217 ref var 279 ref nil cons cons nil cons cons nil cons cons 70 ref "B" 252 remove cons nil cons cons 42 ref cons 186 remove subst subst eqMp nil 103 ref 274 ref "_31711" 271 ref var 285 def 6 ref 276 ref 285 ref varTerm 286 def 17 ref appTerm 287 def appTerm 279 ref appTerm 288 def appTerm 21 ref 22 ref 24 ref 25 ref 276 remove 286 ref 32 ref appTerm 289 def appTerm 245 ref 246 ref 251 ref 257 ref 286 ref 31 ref appTerm 254 ref appTerm 248 ref appTerm appTerm absTerm 259 ref appTerm 290 def absTerm 291 def absTerm 292 def appTerm absTerm 293 def appTerm 294 def absTerm 295 def appTerm 296 def appTerm 297 def absTerm 298 def appTerm 299 def nil cons cons 104 ref 274 remove 285 ref 6 ref 214 ref 245 ref 214 ref 246 ref 209 ref 287 remove 248 ref appTerm 300 def 249 ref appTerm appTerm 301 def 211 ref appTerm 302 def absTerm 303 def appTerm 304 def absTerm 305 def appTerm 306 def appTerm 214 ref 245 ref 214 ref 246 ref 21 ref 22 ref 24 ref 25 ref 209 ref 289 remove 248 ref appTerm 307 def 249 ref appTerm appTerm 308 def 290 remove appTerm 309 def absTerm 310 def appTerm 311 def absTerm 312 def appTerm 313 def absTerm 314 def appTerm 315 def absTerm 316 def appTerm 317 def appTerm 318 def absTerm 319 def appTerm 320 def nil cons 321 def cons nil cons 322 def cons nil cons cons 165 ref subst nil "P" 272 remove var 323 def 285 ref 105 ref 298 ref 286 ref appTerm 324 def appTerm 320 ref appTerm 325 def absTerm nil cons cons nil cons nil cons cons "A" 271 ref nil cons cons nil cons 326 def 42 ref cons 14 ref 171 remove appTerm refl 181 remove appThm 183 remove eqMp sym 327 def subst 328 def subst 285 ref nil 8 ref 325 remove nil cons cons nil cons nil cons cons 137 ref subst nil 103 ref 324 ref nil cons 329 def cons 322 ref cons nil cons cons 330 def 121 ref subst 330 remove 178 ref subst 324 ref betaConv 324 remove assume eqMp nil 103 ref 297 remove nil cons 331 def cons 322 remove cons nil cons cons 332 def 165 ref subst proveHyp 332 ref 121 ref subst 332 remove 178 ref subst 319 ref 286 ref appTerm 333 def betaConv 334 def sym nil 142 ref 288 ref nil cons cons 143 ref 296 remove nil cons 335 def cons nil cons cons nil cons cons 336 def 157 ref subst nil "P" 207 ref var 337 def 305 remove nil cons cons nil cons nil cons cons "A" 202 ref cons 338 def nil cons 339 def 42 ref cons 340 def 327 ref subst 341 def subst 245 ref nil 8 ref 304 remove nil cons cons nil cons nil cons cons 137 ref subst nil 337 ref 303 remove nil cons cons nil cons nil cons cons 341 ref subst 246 ref nil 8 ref 302 remove nil cons cons nil cons nil cons cons 137 ref subst 301 remove refl 278 remove 249 ref appTerm betaConv appThm 226 ref 300 remove appTerm refl 279 remove 248 ref appTerm betaConv appThm 288 remove assume 248 ref refl 342 def appThm eqMp 249 ref refl 343 def appThm eqMp eqMp absThm eqMp eqMp absThm eqMp proveHyp nil 103 ref 306 remove nil cons cons 104 ref 317 remove nil cons cons nil cons cons nil cons cons 178 ref subst proveHyp 336 remove 239 ref subst nil 337 ref 316 remove nil cons cons nil cons nil cons cons 341 ref subst 245 ref nil 8 ref 315 remove nil cons cons nil cons nil cons cons 137 ref subst nil 337 ref 314 remove nil cons cons nil cons nil cons cons 341 ref subst 246 ref nil 8 ref 313 remove nil cons cons nil cons nil cons cons 137 ref subst nil 195 ref 312 remove nil cons cons nil cons nil cons cons 194 ref 42 ref cons 327 ref subst 344 def subst 22 ref nil 8 ref 311 remove nil cons cons nil cons nil cons cons 137 ref subst nil "P" 11 remove var 345 def 310 remove nil cons cons nil cons nil cons cons "A" 27 ref cons 346 def nil cons 347 def 42 ref cons 348 def 327 ref subst 349 def subst 25 ref nil 8 ref 309 remove nil cons cons nil cons nil cons cons 137 ref subst 308 remove refl 291 remove 249 ref appTerm betaConv appThm 226 remove 307 remove appTerm refl 292 remove 248 ref appTerm betaConv appThm 293 ref 31 ref appTerm 350 def betaConv 295 ref 30 ref appTerm 351 def betaConv nil 103 ref 335 remove cons 104 ref 351 remove nil cons cons nil cons cons nil cons cons 165 ref subst 194 ref 195 ref 295 remove nil cons cons 196 ref 30 remove nil cons cons nil cons cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 294 remove nil cons cons 104 ref 350 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 347 ref 345 ref 293 remove nil cons cons "x" 10 ref var 352 def 31 ref nil cons cons nil cons cons nil cons cons 185 ref subst eqMp eqMp 342 ref appThm eqMp 343 ref appThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp proveHyp eqMp eqMp 326 ref 323 ref 319 ref nil cons cons 353 def "x" 271 remove var 354 def 286 ref nil cons cons nil cons cons nil cons cons 14 ref 49 ref 170 ref appTerm 355 def appTerm 356 def refl 51 ref 21 ref 104 ref 105 ref 86 ref 173 ref 105 ref 52 ref 174 ref appTerm 357 def appTerm 358 def 108 ref appTerm absTerm appTerm appTerm 108 ref appTerm absTerm appTerm absTerm 359 def 170 remove appTerm betaConv appThm nil 50 remove 359 remove appTerm axiom 182 remove appThm eqMp 360 def sym nil 195 ref 143 ref 105 ref 86 ref 173 ref 105 ref 175 ref appTerm 361 def 148 ref appTerm 362 def absTerm 363 def appTerm 364 def appTerm 365 def 148 ref appTerm 366 def absTerm nil cons cons nil cons nil cons cons 344 ref subst 143 ref nil 8 ref 366 remove nil cons cons nil cons nil cons cons 137 ref subst nil 103 ref 364 ref nil cons 367 def cons 368 def 104 ref 148 ref nil cons 369 def cons nil cons 370 def cons nil cons cons 371 def 121 ref subst 371 ref 178 ref subst nil 103 ref 176 ref cons 370 ref cons nil cons cons 372 def 165 ref subst 373 def 363 ref 174 ref appTerm 374 def betaConv nil 368 ref 104 ref 374 remove nil cons cons nil cons cons nil cons cons 165 ref subst "A" 53 ref cons 375 def nil cons 376 def 169 ref 363 remove nil cons cons 377 def 173 ref 174 ref nil cons cons nil cons 378 def cons nil cons cons 185 ref subst eqMp eqMp 379 def eqMp eqMp nil 142 ref 367 ref cons 380 def 143 ref 369 ref cons nil cons 381 def cons nil cons cons 157 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp 382 def subst proveHyp eqMp nil 142 ref 331 remove cons 143 ref 321 ref cons nil cons 383 def cons nil cons cons 157 ref subst deductAntisym eqMp eqMp eqMp nil 142 ref 329 remove cons 383 ref cons nil cons cons 157 ref subst deductAntisym eqMp eqMp absThm eqMp nil 103 ref 19 ref 273 remove constTerm 384 def 354 ref 105 ref 298 ref 354 ref varTerm 385 def appTerm appTerm 320 ref appTerm absTerm appTerm nil cons cons 104 ref 105 ref 299 remove appTerm 320 ref appTerm nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 326 ref 323 ref 298 remove nil cons cons 383 remove cons nil cons cons nil 368 ref 104 ref 105 ref 355 ref appTerm 386 def 148 ref appTerm nil cons 387 def cons nil cons cons nil cons cons 388 def 121 ref subst 388 remove 178 ref subst nil 103 ref 355 remove nil cons 389 def cons 390 def 370 ref cons nil cons cons 391 def 121 ref subst 391 remove 178 ref subst 371 remove 165 ref subst 104 ref 105 ref 86 ref 173 ref 361 remove 108 ref appTerm absTerm appTerm appTerm 108 ref appTerm absTerm 392 def 148 ref appTerm 393 def betaConv nil 390 remove 104 ref 21 ref 392 ref appTerm 394 def nil cons 395 def cons nil cons cons nil cons cons 396 def 165 ref subst 360 remove nil 103 ref 356 remove 394 ref appTerm nil cons cons 104 ref 386 remove 394 remove appTerm nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 396 remove nil 103 ref 14 ref 106 ref appTerm 397 def 108 ref appTerm 398 def nil cons 399 def cons 400 def 104 ref 109 ref nil cons 401 def cons nil cons 402 def cons nil cons cons 403 def 121 ref subst 403 remove 178 ref subst 121 ref 178 ref 398 remove assume 404 def 138 remove eqMp eqMp 158 ref deductAntisym eqMp 405 def eqMp nil 142 ref 399 remove cons 406 def 143 ref 401 ref cons nil cons 407 def cons nil cons cons 157 ref subst deductAntisym eqMp 408 def subst eqMp eqMp nil 103 ref 395 remove cons 104 ref 393 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 194 ref 195 ref 392 remove nil cons cons 196 ref 369 remove cons nil cons cons nil cons cons 185 ref subst eqMp eqMp eqMp eqMp nil 142 ref 389 remove cons 381 ref cons nil cons cons 157 ref subst deductAntisym eqMp eqMp nil 380 ref 143 ref 387 remove cons nil cons cons nil cons cons 157 ref subst deductAntisym eqMp 409 def subst eqMp eqMp proveHyp nil 103 ref 321 remove cons 104 ref 48 ref 0 ref 262 ref 2 ref cons opType constTerm 260 ref appTerm 410 def nil cons 411 def cons nil cons 412 def cons nil cons cons 165 ref subst nil 323 remove 285 ref 105 ref 333 ref appTerm 410 ref appTerm 413 def absTerm nil cons cons nil cons nil cons cons 328 remove subst 285 remove nil 8 ref 413 remove nil cons cons nil cons nil cons cons 137 ref subst nil 103 ref 333 ref nil cons 414 def cons 412 ref cons nil cons cons 415 def 121 ref subst 415 remove 178 ref subst 334 remove 333 remove assume eqMp nil 103 ref 318 ref nil cons 416 def cons 412 ref cons nil cons cons 417 def 165 ref subst proveHyp 417 ref 121 ref subst 417 remove 178 ref subst "_31708" 201 ref var 418 def "_31709" 201 ref var 419 def "_31710" 10 ref var 420 def 286 remove 420 ref varTerm appTerm 421 def 418 remove varTerm appTerm 419 ref varTerm 422 def appTerm absTerm absTerm absTerm 423 def refl nil 103 ref 263 remove 423 ref appTerm 423 ref appTerm nil cons cons 412 ref cons nil cons cons 165 ref subst proveHyp nil 244 remove 423 ref nil cons cons nil cons nil cons cons nil 103 ref 264 remove 423 ref appTerm 424 def nil cons 425 def cons 412 remove cons nil cons cons 426 def 121 ref subst 426 remove 178 ref subst 267 remove sym 7 remove 214 ref refl 427 def 245 ref 427 ref 246 ref 209 ref refl 428 def 424 remove assume 429 def 342 ref appThm 423 ref 248 ref appTerm betaConv trans 343 ref appThm 419 ref 420 ref 421 ref 248 ref appTerm 430 def 422 ref appTerm absTerm absTerm 249 ref appTerm betaConv trans 431 def 17 ref refl appThm 420 ref 430 remove 249 ref appTerm absTerm 432 def 17 ref appTerm betaConv trans appThm 211 ref refl appThm absThm appThm absThm appThm appThm 427 ref 245 ref 427 ref 246 ref 60 remove 22 ref 61 remove 25 ref 428 ref 431 remove 32 ref refl appThm 432 remove 32 ref appTerm betaConv trans appThm 251 ref 257 ref refl 429 remove 254 ref refl 433 def appThm 423 remove 254 ref appTerm betaConv trans 342 ref appThm 419 remove 420 ref 421 remove 254 ref appTerm 434 def 422 remove appTerm absTerm absTerm 248 ref appTerm betaConv trans 66 remove appThm 420 remove 434 remove 248 ref appTerm absTerm 31 ref appTerm betaConv trans appThm absThm 259 ref refl 435 def appThm appThm absThm appThm absThm appThm absThm appThm absThm appThm appThm sym 318 remove assume eqMp eqMp 268 remove "P" 262 remove var 260 remove nil cons cons "x" 243 ref var 247 remove nil cons cons nil cons cons nil cons cons 382 ref subst proveHyp eqMp nil 142 ref 425 remove cons 143 ref 411 remove cons nil cons 436 def cons nil cons cons 157 ref subst deductAntisym eqMp subst eqMp eqMp nil 142 ref 416 remove cons 436 ref cons nil cons cons 157 ref subst deductAntisym eqMp eqMp eqMp nil 142 ref 414 remove cons 436 ref cons nil cons cons 157 ref subst deductAntisym eqMp eqMp absThm eqMp nil 103 ref 384 remove 354 remove 105 ref 319 remove 385 remove appTerm appTerm 410 ref appTerm absTerm appTerm nil cons cons 104 ref 105 ref 320 remove appTerm 410 remove appTerm nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 326 remove 353 remove 436 remove cons nil cons cons 409 ref subst eqMp eqMp proveHyp eqMp eqMp defineConstList 437 def pop 438 def pop 437 ref nil 142 ref 214 ref 245 ref 214 ref 246 ref 209 ref 438 remove hdTl pop 243 remove constTerm 439 def 248 ref appTerm 249 ref appTerm 440 def 17 ref appTerm appTerm 211 ref appTerm absTerm appTerm absTerm appTerm 441 def nil cons cons 143 ref 214 ref 245 ref 214 ref 246 ref 21 ref 22 remove 24 ref 25 remove 209 ref 440 remove 32 remove appTerm appTerm 251 ref 257 remove 439 ref 254 ref appTerm 248 ref appTerm 31 remove appTerm appTerm absTerm 259 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 442 def nil cons cons nil cons cons nil cons cons 443 def 157 ref subst proveHyp nil 441 remove thm nil 337 ref 215 ref 13 ref 0 ref 10 ref 40 remove cons opType constTerm 444 def "Number.Natural.Fibonacci.encode" "_31854" 201 ref var 445 def "Number.Natural.Fibonacci.encode.find" "f" 0 ref 201 ref 0 ref 201 ref 0 ref 201 ref 27 ref cons opType 446 def nil cons cons opType 447 def nil cons 448 def cons opType 449 def var 450 def nil cons cons nil cons 450 ref 214 ref 215 ref 214 ref 245 ref 214 ref 246 ref 444 ref 450 ref varTerm 451 def 219 ref appTerm 452 def 248 ref appTerm 249 ref appTerm appTerm 251 ref 33 ref 0 ref 1 ref 0 ref 10 ref 28 remove cons opType nil cons cons opType constTerm 453 def "Number.Natural.<" const 208 ref constTerm 219 ref appTerm 454 def 254 ref appTerm appTerm "Number.Natural.Fibonacci.encode.mk" "mk" 0 ref 10 ref 449 ref nil cons 455 def cons opType 456 def var 457 def nil cons cons nil cons 457 ref 24 ref "l" 10 ref var 458 def 214 ref 215 ref 214 ref 245 ref 214 ref 246 ref 444 ref 457 remove varTerm 459 def 458 ref varTerm 460 def appTerm 219 ref appTerm 248 ref appTerm 249 ref appTerm appTerm 453 ref 209 ref 249 ref appTerm 461 def 211 ref appTerm 462 def appTerm 460 ref appTerm 463 def 453 ref "Number.Natural.<=" const 208 remove constTerm 464 def 248 ref appTerm 219 ref appTerm 465 def appTerm 466 def 459 ref 29 ref 18 ref appTerm 467 def 460 ref appTerm 468 def appTerm "Number.Natural.-" const 217 remove constTerm 469 def 219 ref appTerm 470 def 248 ref appTerm 471 def appTerm 249 ref appTerm 469 ref 248 ref appTerm 472 def 249 ref appTerm 473 def appTerm appTerm 459 ref 29 remove "Data.Bool.F" const 1 ref constTerm 474 def appTerm 475 def 460 ref appTerm 476 def appTerm 219 ref appTerm 249 ref appTerm 473 ref appTerm appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 477 def refl 478 def 13 ref 0 ref 456 ref 0 ref 456 ref 2 ref cons opType 479 def nil cons cons opType constTerm 459 ref appTerm 39 ref 0 ref 479 ref 456 ref nil cons 480 def cons opType constTerm 481 def 477 ref appTerm appTerm assume sym appThm 477 ref 459 remove appTerm betaConv trans "A" 480 remove cons nil cons 482 def 42 ref cons 55 ref subst 478 remove appThm "p" 479 ref var 483 def 483 remove varTerm 484 def 481 remove 484 remove appTerm appTerm absTerm 477 ref appTerm betaConv trans "h" 0 ref "Data.Pair.*" typeOp 485 def 10 ref 485 ref 201 ref 485 ref 203 remove opType 486 def nil cons 487 def cons 488 def opType 489 def nil cons 490 def cons opType 491 def 27 ref cons opType 492 def var 493 def 48 ref 0 ref 0 ref 492 ref 2 ref cons opType 494 def 2 ref cons opType 495 def constTerm 496 def "f" 492 ref var 497 def 19 ref 0 ref 0 ref 491 ref 2 ref cons opType 498 def 2 ref cons opType 499 def constTerm 500 def "x" 491 ref var 501 def 444 ref 497 ref varTerm 502 def 501 ref varTerm 503 def appTerm appTerm 504 def 453 ref 39 ref 0 ref 499 ref 498 ref nil cons 505 def cons opType constTerm 506 def "f" 498 ref var 507 def 214 ref 245 ref 24 ref 458 ref 214 ref 215 ref 214 ref 246 ref 14 ref 507 remove varTerm "Data.Pair.," const 508 def 0 ref 10 ref 0 ref 489 ref 491 ref nil cons 509 def cons opType nil cons cons opType constTerm 510 def 460 ref appTerm 508 ref 0 ref 201 ref 0 ref 486 ref 490 ref cons opType nil cons cons opType constTerm 511 def 219 ref appTerm 512 def 508 ref 0 ref 201 ref 0 ref 488 remove opType 513 def nil cons cons opType constTerm 514 def 248 ref appTerm 249 ref appTerm 515 def appTerm 516 def appTerm 517 def appTerm appTerm 35 ref 462 ref appTerm 518 def appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 519 def 503 ref appTerm appTerm 520 def 502 ref 39 ref 0 ref 0 ref 0 ref 491 ref 509 ref cons opType 521 def 2 ref cons opType 522 def 521 ref nil cons 523 def cons opType constTerm 524 def "f" 521 ref var 525 def 214 ref 245 ref 24 ref 458 ref 214 ref 215 ref 214 ref 246 ref 13 ref 0 ref 491 ref 505 ref cons opType constTerm 526 def 525 remove varTerm 517 ref appTerm appTerm 33 ref 0 ref 1 ref 0 ref 491 ref 523 ref cons opType nil cons cons opType constTerm 527 def 465 ref appTerm 528 def 510 ref 468 ref appTerm 529 def 511 ref 471 ref appTerm 530 def 514 ref 249 ref appTerm 531 def 473 ref appTerm 532 def appTerm appTerm 533 def appTerm 510 ref 476 ref appTerm 534 def 512 ref 532 remove appTerm appTerm 535 def appTerm 536 def appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 537 def 503 ref appTerm 538 def appTerm appTerm 539 def 493 ref varTerm 503 ref appTerm 540 def appTerm appTerm absTerm appTerm absTerm appTerm absTerm 541 def 39 ref 0 ref 494 ref 492 ref nil cons 542 def cons opType constTerm 543 def 497 ref 214 ref 245 ref 24 ref 458 ref 214 ref 215 ref 214 ref 246 ref 444 ref 502 ref 517 ref appTerm appTerm 460 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 544 def appTerm 545 def betaConv "g" 521 ref var 546 def 19 ref 495 remove constTerm 547 def 493 ref 496 ref 497 ref 500 ref 501 ref 504 ref 520 ref 502 remove 546 ref varTerm 503 ref appTerm appTerm 548 def appTerm 540 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 549 def 537 ref appTerm 550 def betaConv "p" 498 ref var 551 def 19 ref 0 ref 522 ref 2 ref cons opType 552 def constTerm 553 def 546 remove 547 ref 493 remove 496 ref 497 ref 500 ref 501 ref 504 ref 453 ref 551 remove varTerm 503 ref appTerm appTerm 548 remove appTerm 540 remove appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 554 def 519 ref appTerm 555 def betaConv "A" 509 ref cons 556 def "B" 27 ref cons nil cons 557 def cons 42 ref cons 558 def nil 19 ref 46 remove constTerm 559 def 51 ref 19 ref 0 ref 0 ref 0 ref 43 ref 53 ref cons opType 560 def 2 ref cons opType 2 ref cons opType constTerm "g" 560 ref var 561 def 19 ref 0 ref 0 ref 0 ref 43 ref 74 ref cons 562 def opType 563 def 2 ref cons opType 564 def 2 ref cons opType 565 def constTerm 566 def "h" 563 ref var 567 def 48 ref 565 remove constTerm 568 def "f" 563 ref var 569 def 86 ref 173 ref 82 ref 569 ref varTerm 570 def 174 ref appTerm 571 def appTerm 33 ref 0 ref 1 ref 0 ref 73 ref 75 ref cons opType nil cons cons opType constTerm 572 def 357 ref appTerm 570 ref 561 remove varTerm 174 ref appTerm appTerm appTerm 567 remove varTerm 174 ref appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm axiom 573 def subst nil 103 ref 19 ref 0 ref 499 ref 2 ref cons opType 574 def constTerm 554 ref appTerm nil cons cons 104 ref 555 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp "A" 505 remove cons nil cons 575 def "P" 499 ref var 576 def 554 remove nil cons cons "x" 498 ref var 577 def 519 remove nil cons cons nil cons cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 553 remove 549 ref appTerm nil cons cons 104 ref 550 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp "A" 523 remove cons nil cons 578 def "P" 522 ref var 579 def 549 remove nil cons cons "x" 521 ref var 580 def 537 remove nil cons cons nil cons cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 547 ref 541 ref appTerm nil cons cons 104 ref 545 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp "A" 542 remove cons nil cons 581 def "P" 494 ref var 582 def 541 remove nil cons cons "x" 492 ref var 583 def 544 ref nil cons cons nil cons cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 496 ref 497 ref 500 ref 501 ref 504 remove 539 remove 544 remove 503 ref appTerm 584 def appTerm appTerm absTerm appTerm absTerm 585 def appTerm 586 def nil cons cons 104 ref 48 ref 0 ref 479 ref 2 ref cons opType constTerm 477 ref appTerm 587 def nil cons 588 def cons nil cons 589 def cons nil cons cons 165 ref subst proveHyp nil 582 ref "mk" 492 ref var 590 def 105 ref 585 ref 590 ref varTerm 591 def appTerm 592 def appTerm 587 ref appTerm 593 def absTerm nil cons cons nil cons nil cons cons 581 ref 42 ref cons 594 def 327 ref subst subst 590 remove nil 8 ref 593 remove nil cons cons nil cons nil cons cons 137 ref subst nil 103 ref 592 ref nil cons 595 def cons 589 ref cons nil cons cons 596 def 121 ref subst 596 remove 178 ref subst 592 ref betaConv 592 remove assume eqMp nil 103 ref 500 remove 501 ref 444 ref 591 ref 503 ref appTerm appTerm 520 remove 591 ref 538 remove appTerm appTerm 584 remove appTerm appTerm absTerm 597 def appTerm nil cons 598 def cons 599 def 589 remove cons nil cons cons 600 def 165 ref subst proveHyp 600 ref 121 ref subst 600 remove 178 ref subst 477 ref 458 ref 215 ref 245 ref 246 ref 591 ref 517 ref appTerm absTerm 601 def absTerm 602 def absTerm 603 def absTerm 604 def appTerm betaConv sym nil 345 ref 458 ref 214 ref 215 ref 214 ref 245 ref 214 ref 246 ref 444 ref 604 ref 460 ref appTerm 605 def 219 ref appTerm 248 ref appTerm 249 ref appTerm appTerm 463 ref 466 ref 604 ref 468 ref appTerm 606 def 471 ref appTerm 249 ref appTerm 473 ref appTerm appTerm 604 ref 476 ref appTerm 607 def 219 ref appTerm 249 ref appTerm 473 ref appTerm appTerm appTerm appTerm 608 def absTerm 609 def appTerm 610 def absTerm 611 def appTerm 612 def absTerm 613 def appTerm 614 def absTerm nil cons cons nil cons nil cons cons 349 ref subst 458 ref nil 8 ref 614 remove nil cons cons nil cons nil cons cons 137 ref subst nil 337 ref 613 remove nil cons cons nil cons nil cons cons 341 ref subst 215 ref nil 8 ref 612 remove nil cons cons nil cons nil cons cons 137 ref subst nil 337 ref 611 remove nil cons cons nil cons nil cons cons 341 ref subst 245 ref nil 8 ref 610 remove nil cons cons nil cons nil cons cons 137 ref subst nil 337 ref 609 remove nil cons cons nil cons nil cons cons 341 ref subst 246 ref nil 8 ref 608 remove nil cons cons nil cons nil cons cons 137 ref subst 444 ref refl 615 def 605 remove betaConv 219 ref refl 616 def appThm 603 remove 219 ref appTerm betaConv trans 342 ref appThm 602 remove 248 ref appTerm betaConv trans 343 ref appThm 601 remove 249 ref appTerm betaConv trans appThm 463 ref refl 466 ref refl 606 remove betaConv 471 ref refl appThm 215 ref 245 ref 246 ref 591 ref 529 ref 516 ref appTerm appTerm absTerm absTerm absTerm 471 ref appTerm betaConv trans 343 ref appThm "f'" 201 ref var 617 def 246 ref 591 ref 529 ref 530 ref 514 ref 617 remove varTerm appTerm 249 ref appTerm appTerm appTerm appTerm absTerm absTerm 249 ref appTerm betaConv trans 473 ref refl 618 def appThm "p'" 201 ref var 619 def 591 ref 529 ref 530 ref 531 remove 619 ref varTerm appTerm 620 def appTerm appTerm appTerm absTerm 473 ref appTerm betaConv trans appThm 607 remove betaConv 616 ref appThm 215 ref 245 ref 246 ref 591 ref 534 ref 516 ref appTerm appTerm absTerm absTerm 621 def absTerm 219 ref appTerm betaConv trans 343 ref appThm 621 remove 249 ref appTerm betaConv trans 618 remove appThm 619 remove 591 ref 534 ref 512 ref 620 remove appTerm appTerm appTerm absTerm 473 ref appTerm betaConv trans appThm appThm appThm sym 615 ref nil 501 ref 517 ref nil cons cons nil cons nil cons cons 597 ref 503 ref appTerm 622 def betaConv nil 599 remove 104 ref 622 remove nil cons cons nil cons cons nil cons cons 165 ref subst 556 remove nil cons "P" 498 ref var 597 remove nil cons cons 501 ref 503 remove nil cons cons nil cons cons nil cons cons 185 ref subst eqMp eqMp subst appThm 463 ref 466 ref 591 ref 533 ref appTerm appTerm 591 ref 535 ref appTerm appTerm 623 def appTerm 624 def refl 625 def appThm sym 615 ref 453 ref refl 626 def 246 ref 14 ref 506 remove "_31748" 498 remove var 627 def 214 ref 245 ref 24 ref 458 ref 214 ref 215 ref 214 ref 246 ref 14 ref 627 remove varTerm 517 ref appTerm appTerm 518 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 628 def appTerm 629 def 517 ref appTerm appTerm 518 ref appTerm absTerm 630 def 249 ref appTerm 631 def betaConv 215 ref 214 ref 630 ref appTerm 632 def absTerm 633 def 219 ref appTerm 634 def betaConv 458 ref 214 ref 633 ref appTerm 635 def absTerm 636 def 460 ref appTerm 637 def betaConv 245 ref 24 ref 636 ref appTerm 638 def absTerm 639 def 248 ref appTerm 640 def betaConv 628 ref 629 remove appTerm 641 def betaConv 628 ref "_31746" 491 ref var 642 def 35 ref 209 ref 39 ref 0 ref 0 ref 0 ref 486 ref 202 ref cons opType 643 def 2 ref cons opType 643 ref nil cons cons opType constTerm 644 def "fn" 643 remove var 645 def 214 ref "a" 201 ref var 646 def 214 ref "b" 201 ref var 647 def 209 ref 645 ref varTerm 514 ref 646 ref varTerm 648 def appTerm 647 ref varTerm 649 def appTerm appTerm appTerm 650 def 649 remove appTerm absTerm appTerm absTerm appTerm absTerm appTerm 651 def 39 ref 0 ref 0 ref 0 ref 489 ref 487 ref cons opType 652 def 2 ref cons opType 652 ref nil cons cons opType constTerm "fn" 652 remove var 653 def 214 ref 646 ref 19 ref 0 ref 0 ref 486 ref 2 ref cons opType 654 def 2 ref cons opType 655 def constTerm 656 def "b" 486 ref var 657 def 13 ref 0 ref 486 ref 654 ref nil cons 658 def cons opType constTerm 659 def 653 remove varTerm 511 ref 648 ref appTerm 657 ref varTerm 660 def appTerm 661 def appTerm appTerm 660 remove appTerm absTerm appTerm absTerm appTerm absTerm appTerm 662 def 39 ref 0 ref 0 ref 0 ref 491 ref 490 ref cons opType 663 def 2 ref cons opType 663 ref nil cons cons opType constTerm "fn" 663 remove var 664 def 24 ref "a" 10 ref var 665 def 19 ref 0 ref 0 ref 489 ref 2 ref cons opType 666 def 2 ref cons opType constTerm 667 def "b" 489 ref var 668 def 13 ref 0 ref 489 ref 666 remove nil cons cons opType constTerm 664 remove varTerm 510 ref 665 ref varTerm 669 def appTerm 668 ref varTerm 670 def appTerm 671 def appTerm appTerm 670 remove appTerm absTerm appTerm absTerm appTerm absTerm appTerm 672 def 642 remove varTerm appTerm appTerm appTerm appTerm 211 ref appTerm appTerm absTerm 673 def appTerm betaConv sym nil 337 ref 245 ref 24 ref 458 ref 214 ref 215 ref 214 ref 246 ref 14 ref 673 ref 517 ref appTerm 674 def appTerm 518 ref appTerm 675 def absTerm 676 def appTerm 677 def absTerm 678 def appTerm 679 def absTerm 680 def appTerm 681 def absTerm nil cons cons nil cons nil cons cons 341 ref subst 245 ref nil 8 ref 681 remove nil cons cons nil cons nil cons cons 137 ref subst nil 345 ref 680 remove nil cons cons nil cons nil cons cons 349 ref subst 458 ref nil 8 ref 679 remove nil cons cons nil cons nil cons cons 137 ref subst nil 337 ref 678 remove nil cons cons nil cons nil cons cons 341 ref subst 215 ref nil 8 ref 677 remove nil cons cons nil cons nil cons cons 137 ref subst nil 337 ref 676 remove nil cons cons nil cons nil cons cons 341 ref subst 246 ref nil 8 ref 675 remove nil cons cons nil cons nil cons cons 137 ref subst 674 remove betaConv 14 ref "_31741" 201 ref var 682 def 35 ref 209 ref 682 remove varTerm appTerm 211 ref appTerm appTerm absTerm 683 def 249 ref appTerm 684 def appTerm refl 683 ref 651 ref 662 ref 672 ref 517 ref appTerm 685 def appTerm 686 def appTerm 687 def appTerm betaConv appThm 145 ref 684 remove betaConv appThm 35 ref 209 ref 687 ref appTerm 211 ref appTerm appTerm refl appThm trans 683 remove refl 461 remove refl 688 def 209 ref "_31736" 489 ref var 689 def 651 ref 662 ref 689 remove varTerm appTerm appTerm absTerm 690 def 516 ref appTerm 691 def appTerm refl 690 ref 685 ref appTerm betaConv appThm 428 ref 691 remove betaConv appThm 687 ref refl appThm trans 690 remove refl nil 668 ref 516 ref nil cons cons 665 ref 460 ref nil cons 692 def cons nil cons cons nil cons cons 693 def 346 remove "B" 490 remove cons nil cons cons 42 ref cons 694 def 84 ref 82 ref 39 ref 0 ref 0 ref 0 ref 485 ref 562 remove opType 695 def 74 ref cons opType 696 def 2 ref cons opType 697 def 696 ref nil cons 698 def cons opType constTerm "fn" 696 remove var 699 def 86 ref "a" 43 ref var 700 def 101 ref 84 ref 82 ref 699 ref varTerm 508 ref 0 ref 43 ref 0 ref 73 ref 695 ref nil cons cons opType nil cons cons opType constTerm 700 ref varTerm 701 def appTerm 85 ref appTerm 702 def appTerm appTerm 703 def 85 ref appTerm absTerm appTerm absTerm appTerm absTerm 704 def appTerm 705 def 702 ref appTerm appTerm 85 ref appTerm absTerm 706 def 85 ref appTerm 707 def betaConv 700 ref 101 ref 706 ref appTerm 708 def absTerm 709 def 701 ref appTerm 710 def betaConv 704 ref 705 remove appTerm 711 def betaConv 48 ref 0 ref 697 ref 2 ref cons opType constTerm 712 def refl 699 remove 86 ref refl 713 def 700 ref 101 ref refl 714 def 84 ref 703 remove refl 700 ref 84 ref 85 ref absTerm 715 def absTerm 716 def 701 ref appTerm betaConv 85 ref refl 717 def appThm 715 remove 85 ref appTerm betaConv trans appThm absThm appThm absThm appThm absThm appThm "C" 74 remove cons nil cons "_1343" 0 ref 43 ref 75 remove cons opType var 716 remove nil cons cons nil cons nil cons cons nil "f" 0 ref 43 ref 0 ref 73 ref "C" varType 718 def nil cons 719 def cons opType nil cons cons opType 720 def var 721 def 700 ref 84 ref "_1343" 720 ref var varTerm 701 ref appTerm 85 ref appTerm 722 def absTerm 723 def absTerm 724 def nil cons cons nil cons nil cons cons 721 ref 48 ref 0 ref 0 ref 0 ref 695 ref 719 remove cons opType 725 def 2 ref cons opType 726 def 2 ref cons opType 727 def constTerm 728 def "fn" 725 ref var 729 def 86 ref 700 ref 101 ref 84 ref 13 ref 0 ref 718 ref 0 ref 718 remove 2 ref cons opType nil cons cons opType constTerm 729 ref varTerm 730 def 702 ref appTerm appTerm 731 def 721 remove varTerm 732 def 701 ref appTerm 85 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 733 def 732 ref appTerm 734 def betaConv nil 19 ref 0 ref 0 ref 720 ref 2 ref cons opType 735 def 2 ref cons opType constTerm 733 ref appTerm 736 def axiom nil 103 ref 736 remove nil cons cons 104 ref 734 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp "A" 720 ref nil cons cons nil cons "P" 735 remove var 733 remove nil cons cons "x" 720 remove var 732 remove nil cons cons nil cons cons nil cons cons 185 ref subst eqMp eqMp subst nil 103 ref 728 ref 729 ref 86 ref 700 ref 101 ref 84 ref 731 ref 724 remove 701 ref appTerm 737 def 85 ref appTerm appTerm absTerm appTerm absTerm appTerm 738 def absTerm 739 def appTerm 740 def nil cons cons 104 ref 728 remove 729 ref 86 ref 700 ref 101 ref 84 ref 731 ref 722 remove appTerm absTerm appTerm absTerm appTerm absTerm 741 def appTerm 742 def nil cons 743 def cons nil cons 744 def cons nil cons cons 165 ref subst nil "P" 726 remove var 745 def 729 ref 105 ref 739 ref 730 ref appTerm 746 def appTerm 742 ref appTerm 747 def absTerm nil cons cons nil cons nil cons cons "A" 725 ref nil cons cons nil cons 748 def 42 ref cons 327 ref subst subst 729 remove nil 8 ref 747 remove nil cons cons nil cons nil cons cons 137 ref subst nil 103 ref 746 ref nil cons 749 def cons 744 ref cons nil cons cons 750 def 121 ref subst 750 remove 178 ref subst 746 ref betaConv 746 remove assume eqMp nil 103 ref 738 ref nil cons 751 def cons 744 remove cons nil cons cons 752 def 165 ref subst proveHyp 752 ref 121 ref subst 752 remove 178 ref subst 741 ref 730 ref appTerm betaConv sym 713 ref 700 ref 714 ref 84 ref 731 remove refl 737 remove betaConv 717 ref appThm 723 remove 85 ref appTerm betaConv trans appThm absThm appThm absThm appThm 738 remove assume eqMp eqMp 748 ref 745 ref 741 remove nil cons cons "x" 725 remove var 753 def 730 remove nil cons cons nil cons cons nil cons cons 382 ref subst proveHyp eqMp nil 142 ref 751 remove cons 143 ref 743 remove cons nil cons 754 def cons nil cons cons 157 ref subst deductAntisym eqMp eqMp eqMp nil 142 ref 749 remove cons 754 ref cons nil cons cons 157 ref subst deductAntisym eqMp eqMp absThm eqMp nil 103 ref 19 ref 727 remove constTerm 753 ref 105 ref 739 ref 753 remove varTerm appTerm appTerm 742 ref appTerm absTerm appTerm nil cons cons 104 ref 105 ref 740 remove appTerm 742 remove appTerm nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 748 remove 745 remove 739 remove nil cons cons 754 remove cons nil cons cons 409 ref subst eqMp eqMp proveHyp 755 def subst eqMp nil 103 ref 712 remove 704 ref appTerm nil cons cons 104 ref 711 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp "A" 698 remove cons nil cons "p" 697 remove var 704 remove nil cons cons nil cons nil cons cons nil 103 ref 49 ref 52 ref appTerm 756 def nil cons 757 def cons 758 def 104 ref 14 ref 54 ref appTerm 759 def 18 ref appTerm 760 def nil cons 761 def cons nil cons 762 def cons nil cons cons 763 def 121 ref subst 763 remove 178 ref subst 49 ref refl nil "t" 44 ref var 52 ref nil cons 764 def cons nil cons nil cons cons 375 remove 71 remove cons 42 ref cons "t" 563 ref var 765 def 13 ref 0 ref 563 ref 564 ref nil cons cons opType constTerm 173 ref 765 remove varTerm 766 def 174 ref appTerm absTerm appTerm 766 ref appTerm absTerm 767 def 766 ref appTerm 768 def betaConv nil 566 ref 767 ref appTerm 769 def axiom nil 103 ref 769 remove nil cons cons 104 ref 768 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp "A" 563 ref nil cons cons nil cons 770 def "P" 564 remove var 771 def 767 remove nil cons cons "x" 563 remove var 772 def 766 remove nil cons cons nil cons cons nil cons cons 185 ref subst eqMp eqMp subst subst appThm nil 8 ref 757 ref cons nil cons nil cons cons 773 def 137 ref subst 756 ref assume eqMp trans sym 136 ref eqMp nil 103 ref 49 ref 173 ref 357 ref absTerm appTerm nil cons cons 762 ref cons nil cons cons 165 ref subst proveHyp nil 169 ref 764 ref cons 143 ref 761 remove cons nil cons 774 def cons nil cons cons nil 368 remove 104 ref 105 ref 49 ref 173 ref 175 ref absTerm 775 def appTerm 776 def appTerm 148 ref appTerm 777 def nil cons 778 def cons nil cons 779 def cons nil cons cons 780 def 405 remove nil 103 ref 401 ref cons 781 def 104 ref 105 ref 108 ref appTerm 782 def 106 ref appTerm nil cons 783 def cons nil cons 784 def cons nil cons cons 178 ref subst proveHyp 782 ref refl 404 remove appThm sym nil 103 ref 139 ref cons 785 def 104 ref 139 ref cons nil cons 786 def cons nil cons cons 787 def 121 ref subst 787 remove 178 ref subst 140 remove eqMp nil 142 ref 139 remove cons 144 ref cons nil cons cons 157 ref subst deductAntisym eqMp eqMp 788 def eqMp nil 785 ref 104 ref 132 ref cons nil cons 789 def cons nil cons cons 165 ref subst nil 142 ref 401 remove cons 790 def 143 ref 783 remove cons nil cons 791 def cons nil cons cons 792 def 239 ref subst eqMp 165 ref 792 remove 157 ref subst eqMp deductAntisym deductAntisym 793 def subst 780 ref 121 ref subst 780 remove 178 ref subst nil 169 ref 173 ref 105 ref 775 ref 174 ref appTerm 794 def appTerm 148 ref appTerm 795 def absTerm 796 def nil cons cons nil cons nil cons cons 327 ref subst 173 ref nil 8 ref 795 remove nil cons cons nil cons nil cons cons 137 ref subst nil 103 ref 794 ref nil cons 797 def cons 370 ref cons nil cons cons 798 def 121 ref subst 798 remove 178 ref subst 794 ref betaConv 799 def 794 remove assume eqMp 373 remove proveHyp 379 remove eqMp eqMp nil 142 ref 797 remove cons 381 ref cons nil cons cons 157 ref subst deductAntisym eqMp eqMp absThm eqMp nil 103 ref 86 ref 796 remove appTerm nil cons cons 779 remove cons nil cons cons 165 ref subst proveHyp 376 ref 169 ref 775 remove nil cons cons 800 def 381 ref cons nil cons cons 409 ref subst eqMp eqMp nil 380 remove 143 ref 778 ref cons nil cons cons nil cons cons 157 ref subst deductAntisym eqMp nil 103 ref 365 remove 777 ref appTerm nil cons cons 104 ref 105 ref 777 ref appTerm 364 remove appTerm nil cons cons nil cons cons nil cons cons 178 ref subst proveHyp nil 103 ref 778 ref cons 104 ref 367 ref cons nil cons cons nil cons cons 801 def 121 ref subst 801 remove 178 ref subst nil 377 remove nil cons nil cons cons 327 ref subst 173 ref nil 8 ref 362 remove nil cons cons nil cons nil cons cons 137 ref subst 372 ref 121 ref subst 372 remove 178 ref subst 799 remove sym 175 remove assume eqMp 376 ref 800 remove 378 ref cons nil cons cons 382 ref subst proveHyp nil 103 ref 776 remove nil cons cons 370 remove cons nil cons cons 165 ref subst 777 remove assume eqMp proveHyp eqMp nil 142 ref 176 remove cons 381 remove cons nil cons cons 157 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp nil 142 ref 778 remove cons 143 ref 367 remove cons nil cons cons nil cons cons 157 ref subst deductAntisym eqMp eqMp eqMp subst nil 169 ref 173 ref 358 ref 760 ref appTerm 802 def absTerm nil cons cons nil cons nil cons cons 327 ref subst 173 ref nil 8 ref 802 remove nil cons cons nil cons nil cons cons 137 ref subst nil 103 ref 357 remove nil cons 803 def cons 804 def 762 remove cons nil cons cons 805 def 121 ref subst 805 remove 178 ref subst nil 8 ref 54 ref nil cons 806 def cons nil cons nil cons cons 137 ref subst nil 804 remove 104 ref 806 remove cons 807 def nil cons cons nil cons cons 165 ref subst 173 ref 358 remove 54 ref appTerm absTerm 808 def 174 ref appTerm 809 def betaConv 51 remove 86 ref 808 ref appTerm 810 def absTerm 811 def 52 remove appTerm 812 def betaConv nil 559 remove 811 ref appTerm 813 def axiom nil 103 ref 813 remove nil cons cons 104 ref 812 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp "A" 44 ref nil cons 814 def cons nil cons "P" 45 remove var 811 remove nil cons cons "x" 44 remove var 764 remove cons nil cons cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 810 remove nil cons cons 104 ref 809 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 376 ref 169 ref 808 remove nil cons cons 378 ref cons nil cons cons 185 ref subst eqMp eqMp eqMp eqMp eqMp nil 142 ref 803 remove cons 774 ref cons nil cons cons 157 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp eqMp eqMp nil 142 ref 757 ref cons 774 remove cons nil cons cons 157 ref subst deductAntisym eqMp nil 103 ref 105 ref 756 ref appTerm 815 def 760 remove appTerm nil cons cons 104 ref 14 ref 815 ref 54 remove appTerm appTerm 816 def 815 ref 18 ref appTerm appTerm nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp nil "q'" 1 ref var 817 def 69 remove cons nil cons nil cons cons 756 ref refl nil 103 ref 14 ref 756 ref appTerm 818 def 756 remove appTerm nil cons cons 104 ref 105 ref 815 ref 759 remove 817 ref varTerm 819 def appTerm 820 def appTerm appTerm 816 ref 815 remove 819 ref appTerm appTerm appTerm nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp nil "p'" 1 ref var 821 def 757 remove cons nil cons nil cons cons 817 ref 105 ref 818 remove 821 ref varTerm 822 def appTerm appTerm 105 ref 105 ref 822 ref appTerm 823 def 820 remove appTerm appTerm 816 remove 823 ref 819 ref appTerm 824 def appTerm appTerm appTerm absTerm 825 def 819 ref appTerm 826 def betaConv 821 ref 21 ref 825 ref appTerm 827 def absTerm 828 def 822 ref appTerm 829 def betaConv nil 807 remove 758 remove nil cons cons nil cons cons nil 195 ref 821 ref 21 ref 817 ref 105 ref 397 remove 822 ref appTerm 830 def appTerm 105 ref 823 ref 14 ref 108 ref appTerm 819 ref appTerm 831 def appTerm 832 def appTerm 110 remove 824 ref appTerm 833 def appTerm 834 def appTerm 835 def absTerm 836 def appTerm 837 def absTerm nil cons cons nil cons nil cons cons 344 ref subst 821 remove nil 8 ref 837 remove nil cons cons nil cons nil cons cons 137 ref subst nil 195 ref 836 remove nil cons cons nil cons nil cons cons 344 ref subst 817 remove nil 8 ref 835 remove nil cons cons nil cons nil cons cons 137 ref subst nil 103 ref 830 remove nil cons 838 def cons 839 def 104 ref 834 remove nil cons 840 def cons nil cons cons nil cons cons 841 def 121 ref subst 841 remove 178 ref subst nil 103 ref 832 ref nil cons 842 def cons 104 ref 833 remove nil cons 843 def cons nil cons cons nil cons cons 844 def 121 ref subst 844 remove 178 ref subst nil 781 remove 104 ref 824 ref nil cons 845 def cons nil cons cons nil cons cons 846 def 793 remove subst 846 ref 121 ref subst 846 remove 178 ref subst nil 103 ref 822 ref nil cons 847 def cons 848 def 104 ref 819 ref nil cons 849 def cons nil cons 850 def cons nil cons cons 851 def 121 ref subst 851 ref 178 ref subst nil 839 ref 104 ref 107 ref 822 remove appTerm 852 def nil cons 853 def cons nil cons cons nil cons cons 165 ref subst nil 103 ref 132 remove cons 104 ref 847 ref cons nil cons cons nil cons cons 854 def 408 ref subst eqMp 855 def nil 103 ref 853 ref cons 856 def 850 ref cons nil cons cons 857 def 165 ref subst proveHyp nil 839 remove 104 ref 823 remove 106 remove appTerm 858 def nil cons 859 def cons nil cons cons nil cons cons 165 ref subst 854 ref nil 400 remove 784 remove cons nil cons cons 860 def 121 ref subst 860 remove 178 ref subst 788 remove eqMp nil 406 remove 791 remove cons nil cons cons 157 ref subst deductAntisym eqMp 861 def subst eqMp 862 def nil 103 ref 859 ref cons 863 def 104 ref 105 ref 852 ref appTerm 864 def 819 ref appTerm nil cons 865 def cons nil cons cons nil cons cons 866 def 165 ref subst proveHyp 866 ref 121 ref subst 866 remove 178 ref subst 857 ref 121 ref subst 857 remove 178 ref subst nil 848 ref 789 remove cons nil cons cons 165 ref subst 858 remove assume eqMp 867 def 854 remove 165 ref subst 852 remove assume eqMp 868 def 867 remove proveHyp proveHyp nil 848 remove 104 ref 831 remove nil cons 869 def cons nil cons cons nil cons cons 165 ref subst 832 remove assume eqMp 870 def nil 103 ref 869 remove cons 871 def 104 ref 782 ref 819 ref appTerm 872 def nil cons 873 def cons nil cons cons nil cons cons 165 ref subst proveHyp nil 785 remove 850 ref cons nil cons cons 874 def 408 remove subst eqMp 875 def nil 103 ref 873 ref cons 876 def 850 remove cons nil cons cons 877 def 165 ref subst proveHyp 870 remove nil 871 remove 104 ref 105 ref 819 ref appTerm 108 ref appTerm 878 def nil cons 879 def cons nil cons cons nil cons cons 165 ref subst proveHyp 874 ref 861 remove subst eqMp 880 def nil 103 ref 879 ref cons 881 def 104 ref 105 ref 872 ref appTerm 882 def 819 remove appTerm nil cons 883 def cons nil cons cons nil cons cons 884 def 165 ref subst proveHyp 884 ref 121 ref subst 884 remove 178 ref subst 877 ref 121 ref subst 877 remove 178 ref subst 164 remove 874 remove 165 ref subst 872 remove assume eqMp proveHyp eqMp nil 142 ref 873 remove cons 885 def 143 ref 849 ref cons nil cons 886 def cons nil cons cons 157 ref subst deductAntisym eqMp eqMp nil 142 ref 879 remove cons 887 def 143 ref 883 remove cons nil cons cons nil cons cons 157 ref subst deductAntisym eqMp eqMp eqMp proveHyp eqMp nil 142 ref 853 remove cons 888 def 886 ref cons nil cons cons 157 ref subst deductAntisym eqMp eqMp nil 142 ref 859 remove cons 889 def 143 ref 865 remove cons nil cons cons nil cons cons 157 ref subst deductAntisym eqMp eqMp eqMp eqMp nil 142 ref 847 ref cons 886 remove cons nil cons cons 157 ref subst deductAntisym eqMp eqMp nil 790 remove 143 ref 845 ref cons nil cons cons nil cons cons 157 ref subst deductAntisym eqMp nil 103 ref 105 ref 109 ref appTerm 824 ref appTerm nil cons cons 104 ref 105 ref 824 ref appTerm 109 remove appTerm nil cons cons nil cons cons nil cons cons 178 ref subst proveHyp nil 103 ref 845 ref cons 402 remove cons nil cons cons 890 def 121 ref subst 890 remove 178 ref subst 121 ref 178 ref 855 remove nil 856 remove 786 ref cons nil cons cons 891 def 165 ref subst proveHyp 862 remove nil 863 remove 104 ref 864 remove 108 ref appTerm nil cons 892 def cons nil cons cons nil cons cons 893 def 165 ref subst proveHyp 893 ref 121 ref subst 893 remove 178 ref subst 891 ref 121 ref subst 891 remove 178 ref subst 868 remove 875 remove nil 876 remove 786 ref cons nil cons cons 894 def 165 ref subst proveHyp 880 remove nil 881 remove 104 ref 882 remove 108 remove appTerm nil cons 895 def cons nil cons cons nil cons cons 896 def 165 ref subst proveHyp 896 ref 121 ref subst 896 remove 178 ref subst 894 ref 121 ref subst 894 remove 178 ref subst 851 remove 165 ref subst 824 remove assume eqMp nil 103 ref 849 ref cons 786 remove cons nil cons cons 165 ref subst 878 remove assume eqMp proveHyp eqMp nil 885 remove 144 ref cons nil cons cons 157 ref subst deductAntisym eqMp eqMp nil 887 remove 143 ref 895 remove cons nil cons cons nil cons cons 157 ref subst deductAntisym eqMp eqMp eqMp proveHyp eqMp nil 888 remove 144 remove cons nil cons cons 157 ref subst deductAntisym eqMp eqMp nil 889 remove 143 ref 892 remove cons nil cons cons nil cons cons 157 ref subst deductAntisym eqMp eqMp eqMp eqMp 158 remove deductAntisym eqMp eqMp nil 142 ref 845 remove cons 407 remove cons nil cons cons 157 ref subst deductAntisym eqMp eqMp eqMp eqMp nil 142 ref 842 remove cons 143 ref 843 remove cons nil cons cons nil cons cons 157 ref subst deductAntisym eqMp eqMp nil 142 ref 838 remove cons 143 ref 840 remove cons nil cons cons nil cons cons 157 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp absThm eqMp subst nil 103 ref 21 ref 828 ref appTerm nil cons cons 104 ref 829 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 194 ref 195 ref 828 remove nil cons cons 196 ref 847 remove cons nil cons cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 827 remove nil cons cons 104 ref 826 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 194 ref 195 ref 825 remove nil cons cons 196 ref 849 remove cons nil cons cons nil cons cons 185 ref subst eqMp eqMp subst eqMp subst eqMp 773 remove 8 ref 14 ref 105 ref 133 ref appTerm 18 ref appTerm appTerm 18 ref appTerm absTerm 897 def 133 remove appTerm 898 def betaConv nil 21 ref 897 ref appTerm 899 def axiom nil 103 ref 899 remove nil cons cons 104 ref 898 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 194 ref 195 ref 897 remove nil cons cons 197 remove cons nil cons cons 185 ref subst eqMp eqMp subst trans sym 136 ref eqMp 900 def subst eqMp eqMp nil 103 ref 86 ref 709 ref appTerm nil cons cons 104 ref 710 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 376 ref 169 ref 709 remove nil cons cons 173 ref 701 ref nil cons cons nil cons 901 def cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 708 remove nil cons cons 104 ref 707 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 166 ref 167 ref 706 remove nil cons cons 168 ref cons nil cons cons 185 ref subst eqMp eqMp sym 902 def subst subst 903 def appThm eqMp appThm 688 ref 209 ref "_31730" 486 ref var 904 def 651 ref 904 remove varTerm appTerm absTerm 905 def 515 ref appTerm 906 def appTerm refl 905 ref 662 ref 516 ref appTerm 907 def appTerm betaConv appThm 428 ref 906 remove betaConv appThm 651 ref 907 ref appTerm refl appThm trans 905 remove refl nil 657 ref 515 ref nil cons 908 def cons 646 ref 219 ref nil cons 909 def cons nil cons 910 def cons nil cons cons 911 def 338 ref "B" 487 ref cons nil cons cons 42 ref cons 912 def 902 ref subst subst 913 def appThm eqMp appThm nil 647 ref 249 ref nil cons 914 def cons 646 ref 248 ref nil cons 915 def cons nil cons 916 def cons nil cons cons 917 def 338 ref "B" 202 ref cons nil cons 918 def cons 42 ref cons 919 def 902 ref subst subst 920 def eqMp eqMp 921 def appThm eqMp sym trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp 575 ref 576 remove 628 ref nil cons 922 def cons 577 remove 673 remove nil cons cons nil cons cons nil cons cons 382 ref subst proveHyp nil 103 ref 48 ref 574 remove constTerm 628 remove appTerm nil cons cons 104 ref 641 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp nil "p" 499 remove var 922 remove cons nil cons nil cons cons 575 remove 42 ref cons 900 ref subst subst eqMp eqMp nil 103 ref 214 ref 639 ref appTerm nil cons cons 104 ref 640 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 339 ref 337 ref 639 remove nil cons cons "x" 201 ref var 923 def 915 remove cons nil cons 924 def cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 638 remove nil cons cons 104 ref 637 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 347 ref 345 ref 636 remove nil cons cons 352 ref 692 ref cons nil cons 925 def cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 635 remove nil cons cons 104 ref 634 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 339 ref 337 ref 633 remove nil cons cons 923 ref 909 ref cons nil cons 926 def cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 632 remove nil cons cons 104 ref 631 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 339 ref 337 ref 630 remove nil cons cons 923 ref 914 ref cons nil cons 927 def cons nil cons cons 185 ref subst eqMp eqMp appThm 591 ref refl 246 ref 526 ref 524 remove "_31778" 521 remove var 928 def 214 ref 245 ref 24 ref 458 ref 214 ref 215 ref 214 ref 246 ref 526 ref 928 remove varTerm 517 ref appTerm appTerm 536 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 929 def appTerm 930 def 517 ref appTerm appTerm 536 ref appTerm absTerm 931 def 249 ref appTerm 932 def betaConv 215 ref 214 ref 931 ref appTerm 933 def absTerm 934 def 219 ref appTerm 935 def betaConv 458 ref 214 ref 934 ref appTerm 936 def absTerm 937 def 460 ref appTerm 938 def betaConv 245 ref 24 ref 937 ref appTerm 939 def absTerm 940 def 248 ref appTerm 941 def betaConv 929 ref 930 remove appTerm 942 def betaConv 929 ref "_31776" 491 ref var 943 def 527 ref 464 ref 644 remove 645 remove 214 ref 646 ref 214 ref 647 remove 650 remove 648 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm 944 def 662 ref 672 remove 943 remove varTerm 945 def appTerm 946 def appTerm 947 def appTerm 948 def appTerm 39 ref 0 ref 0 ref 0 ref 489 ref 202 ref cons opType 949 def 2 ref cons opType 949 ref nil cons cons opType constTerm "fn" 949 remove var 950 def 214 ref 646 ref 656 ref 657 remove 209 ref 950 remove varTerm 661 remove appTerm appTerm 648 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm 951 def 946 remove appTerm 952 def appTerm appTerm 510 ref 467 ref 543 ref "fn" 492 ref var 953 def 24 ref 665 remove 667 remove 668 remove 444 ref 953 remove varTerm 671 remove appTerm appTerm 669 remove appTerm absTerm appTerm absTerm appTerm absTerm appTerm 954 def 945 remove appTerm 955 def appTerm appTerm 511 ref 469 ref 952 ref appTerm 948 ref appTerm appTerm 514 ref 651 ref 947 remove appTerm 956 def appTerm 469 ref 948 remove appTerm 956 remove appTerm appTerm 957 def appTerm appTerm appTerm 510 ref 475 ref 955 remove appTerm appTerm 511 ref 952 remove appTerm 957 remove appTerm appTerm appTerm absTerm 958 def appTerm betaConv sym nil 337 ref 245 ref 24 ref 458 ref 214 ref 215 ref 214 ref 246 ref 526 ref 958 ref 517 ref appTerm 959 def appTerm 536 ref appTerm 960 def absTerm 961 def appTerm 962 def absTerm 963 def appTerm 964 def absTerm 965 def appTerm 966 def absTerm nil cons cons nil cons nil cons cons 341 ref subst 245 ref nil 8 ref 966 remove nil cons cons nil cons nil cons cons 137 ref subst nil 345 ref 965 remove nil cons cons nil cons nil cons cons 349 ref subst 458 ref nil 8 ref 964 remove nil cons cons nil cons nil cons cons 137 ref subst nil 337 ref 963 remove nil cons cons nil cons nil cons cons 341 ref subst 215 ref nil 8 ref 962 remove nil cons cons nil cons nil cons cons 137 ref subst nil 337 ref 961 remove nil cons cons nil cons nil cons cons 341 ref subst 246 ref nil 8 ref 960 remove nil cons cons nil cons nil cons cons 137 ref subst 959 remove betaConv 526 ref "_31771" 201 ref var 967 def 528 remove 529 ref 530 remove 514 ref 967 ref varTerm 968 def appTerm 969 def 472 remove 968 ref appTerm appTerm 970 def appTerm appTerm appTerm 534 ref 512 ref 970 remove appTerm appTerm appTerm absTerm 249 ref appTerm 971 def appTerm refl 967 ref 527 ref 464 ref 944 ref 686 remove appTerm 972 def appTerm 951 ref 685 ref appTerm 973 def appTerm appTerm 974 def 510 ref 467 ref 954 ref 517 ref appTerm 975 def appTerm appTerm 976 def 511 ref 469 ref 973 ref appTerm 977 def 972 ref appTerm appTerm 978 def 969 ref 469 ref 972 ref appTerm 979 def 968 ref appTerm appTerm 980 def appTerm appTerm appTerm 510 ref 475 ref 975 ref appTerm appTerm 981 def 511 ref 973 ref appTerm 982 def 980 remove appTerm appTerm appTerm absTerm 983 def 687 ref appTerm betaConv appThm 526 remove refl 971 remove betaConv appThm 974 remove 976 ref 978 remove 514 ref 687 ref appTerm 979 remove 687 remove appTerm appTerm 984 def appTerm appTerm appTerm 981 ref 982 ref 984 remove appTerm appTerm appTerm refl appThm trans 13 ref 0 ref 0 ref 201 ref 509 remove cons opType 985 def 0 ref 985 ref 2 ref cons opType nil cons cons opType constTerm 986 def "_31770" 201 ref var 987 def 967 ref 527 ref 464 remove 987 ref varTerm 988 def appTerm 989 def 219 ref appTerm appTerm 529 ref 511 ref 470 remove 988 ref appTerm appTerm 969 remove 469 ref 988 ref appTerm 968 remove appTerm appTerm 990 def appTerm appTerm appTerm 534 ref 512 remove 990 ref appTerm appTerm appTerm absTerm absTerm 248 ref appTerm 991 def appTerm refl 987 ref 967 ref 527 ref 989 ref 973 ref appTerm appTerm 976 ref 511 ref 977 remove 988 ref appTerm appTerm 990 ref appTerm appTerm appTerm 981 ref 982 remove 990 ref appTerm appTerm appTerm absTerm absTerm 992 def 972 ref appTerm betaConv appThm 986 remove refl 991 remove betaConv appThm 983 remove refl appThm trans 13 ref 0 ref 0 ref 201 ref 985 remove nil cons cons opType 993 def 0 ref 993 ref 2 ref cons opType nil cons cons opType constTerm 994 def "_31769" 201 ref var 995 def 987 ref 967 ref 527 remove 989 remove 995 ref varTerm 996 def appTerm appTerm 997 def 529 remove 511 ref 469 ref 996 ref appTerm 988 remove appTerm appTerm 990 ref appTerm 998 def appTerm appTerm 534 remove 511 remove 996 remove appTerm 990 remove appTerm 999 def appTerm appTerm absTerm absTerm absTerm 219 ref appTerm 1000 def appTerm refl 995 ref 987 ref 967 ref 997 ref 976 remove 998 ref appTerm appTerm 981 remove 999 ref appTerm appTerm absTerm absTerm absTerm 1001 def 973 ref appTerm betaConv appThm 994 remove refl 1000 remove betaConv appThm 992 remove refl appThm trans 13 ref 0 ref 0 ref 201 ref 993 remove nil cons cons opType 1002 def 0 ref 1002 remove 2 ref cons opType nil cons cons opType constTerm 1003 def "_31768" 10 ref var 1004 def 995 remove 987 remove 967 remove 997 remove 510 ref 467 remove 1004 remove varTerm 1005 def appTerm appTerm 998 remove appTerm appTerm 510 remove 475 remove 1005 remove appTerm appTerm 999 remove appTerm appTerm absTerm absTerm absTerm absTerm 1006 def 460 ref appTerm 1007 def appTerm refl 1006 ref 975 remove appTerm betaConv appThm 1003 remove refl 1007 remove betaConv appThm 1001 remove refl appThm trans 1006 remove refl 693 remove 694 remove 84 ref 13 ref 0 ref 43 ref 814 remove cons opType constTerm 1008 def 39 ref 0 ref 0 ref 0 ref 695 ref 53 ref cons opType 1009 def 2 ref cons opType 1010 def 1009 ref nil cons 1011 def cons opType constTerm "fn" 1009 remove var 1012 def 86 ref 700 ref 101 ref 84 ref 1008 ref 1012 ref varTerm 702 ref appTerm appTerm 1013 def 701 ref appTerm absTerm appTerm absTerm appTerm absTerm 1014 def appTerm 1015 def 702 ref appTerm appTerm 701 ref appTerm absTerm 1016 def 85 ref appTerm 1017 def betaConv 700 ref 101 remove 1016 ref appTerm 1018 def absTerm 1019 def 701 ref appTerm 1020 def betaConv 1014 ref 1015 remove appTerm 1021 def betaConv 48 ref 0 ref 1010 ref 2 ref cons opType constTerm 1022 def refl 1012 remove 713 remove 700 ref 714 remove 84 ref 1013 remove refl 700 ref 84 ref 701 ref absTerm 1023 def absTerm 1024 def 701 remove appTerm betaConv 717 remove appThm 1023 remove 85 remove appTerm betaConv trans appThm absThm appThm absThm appThm absThm appThm "C" 53 ref cons nil cons "_1343" 0 ref 43 ref 0 ref 73 ref 53 ref cons opType nil cons cons opType var 1024 remove nil cons cons nil cons nil cons cons 755 remove subst eqMp nil 103 ref 1022 remove 1014 ref appTerm nil cons cons 104 ref 1021 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp "A" 1011 remove cons nil cons "p" 1010 remove var 1014 remove nil cons cons nil cons nil cons cons 900 ref subst eqMp eqMp nil 103 ref 86 ref 1019 ref appTerm nil cons cons 104 ref 1020 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 376 ref 169 ref 1019 remove nil cons cons 901 remove cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 1018 remove nil cons cons 104 ref 1017 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 166 remove 167 remove 1016 remove nil cons cons 168 remove cons nil cons cons 185 ref subst eqMp eqMp sym 1025 def subst subst 1026 def appThm eqMp 209 ref 219 ref appTerm refl 1027 def 209 ref "_31732" 489 ref var 1028 def 951 remove 1028 remove varTerm appTerm absTerm 1029 def 516 ref appTerm 1030 def appTerm refl 1029 ref 685 ref appTerm betaConv appThm 428 ref 1030 remove betaConv appThm 973 remove refl appThm trans 1029 remove refl 903 ref appThm eqMp appThm 911 remove 912 remove 1025 ref subst subst eqMp appThm eqMp 209 ref 248 ref appTerm refl 1031 def 209 ref "_31734" 489 remove var 1032 def 944 ref 662 remove 1032 remove varTerm appTerm appTerm absTerm 1033 def 516 remove appTerm 1034 def appTerm refl 1033 ref 685 remove appTerm betaConv appThm 428 ref 1034 remove betaConv appThm 972 remove refl appThm trans 1033 remove refl 903 remove appThm eqMp appThm 1031 ref 209 ref "_31728" 486 ref var 1035 def 944 ref 1035 remove varTerm appTerm absTerm 1036 def 515 ref appTerm 1037 def appTerm refl 1036 ref 907 ref appTerm betaConv appThm 428 ref 1037 remove betaConv appThm 944 ref 907 remove appTerm refl appThm trans 1036 remove refl 913 remove appThm eqMp appThm 917 remove 919 remove 1025 ref subst subst 1038 def eqMp eqMp appThm eqMp 921 remove appThm eqMp sym trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp 578 ref 579 remove 929 ref nil cons 1039 def cons 580 remove 958 remove nil cons cons nil cons cons nil cons cons 382 ref subst proveHyp nil 103 ref 48 ref 552 remove constTerm 929 remove appTerm nil cons cons 104 ref 942 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp nil "p" 522 remove var 1039 remove cons nil cons nil cons cons 578 remove 42 ref cons 900 ref subst subst eqMp eqMp nil 103 ref 214 ref 940 ref appTerm nil cons cons 104 ref 941 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 339 ref 337 ref 940 remove nil cons cons 924 ref cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 939 remove nil cons cons 104 ref 938 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 347 ref 345 ref 937 remove nil cons cons 925 ref cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 936 remove nil cons cons 104 ref 935 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 339 ref 337 ref 934 remove nil cons cons 926 ref cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 933 remove nil cons cons 104 ref 932 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 339 ref 337 ref 931 remove nil cons cons 927 ref cons nil cons cons 185 ref subst eqMp eqMp appThm appThm 246 ref 444 ref 543 remove "_31808" 492 remove var 1040 def 214 ref 245 ref 24 ref 458 ref 214 ref 215 ref 214 ref 246 ref 444 ref 1040 remove varTerm 517 ref appTerm appTerm 460 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 1041 def appTerm 1042 def 517 ref appTerm appTerm 460 ref appTerm absTerm 1043 def 249 ref appTerm 1044 def betaConv 215 ref 214 ref 1043 ref appTerm 1045 def absTerm 1046 def 219 ref appTerm 1047 def betaConv 458 ref 214 ref 1046 ref appTerm 1048 def absTerm 1049 def 460 ref appTerm 1050 def betaConv 245 ref 24 ref 1049 ref appTerm 1051 def absTerm 1052 def 248 ref appTerm 1053 def betaConv 1041 ref 1042 remove appTerm 1054 def betaConv 1041 ref "_31806" 491 ref var 1055 def 954 remove 1055 remove varTerm appTerm absTerm 1056 def appTerm betaConv sym nil 337 ref 245 ref 24 ref 458 ref 214 ref 215 ref 214 ref 246 ref 444 ref 1056 ref 517 remove appTerm 1057 def appTerm 460 ref appTerm 1058 def absTerm 1059 def appTerm 1060 def absTerm 1061 def appTerm 1062 def absTerm 1063 def appTerm 1064 def absTerm nil cons cons nil cons nil cons cons 341 ref subst 245 ref nil 8 ref 1064 remove nil cons cons nil cons nil cons cons 137 ref subst nil 345 ref 1063 remove nil cons cons nil cons nil cons cons 349 ref subst 458 ref nil 8 ref 1062 remove nil cons cons nil cons nil cons cons 137 ref subst nil 337 ref 1061 remove nil cons cons nil cons nil cons cons 341 ref subst 215 ref nil 8 ref 1060 remove nil cons cons nil cons nil cons cons 137 ref subst nil 337 ref 1059 remove nil cons cons nil cons nil cons cons 341 ref subst 246 ref nil 8 ref 1058 remove nil cons cons nil cons nil cons cons 137 ref subst 1057 remove betaConv 1026 remove sym trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp 581 ref 582 ref 1041 ref nil cons 1065 def cons 583 ref 1056 remove nil cons cons nil cons cons nil cons cons 382 ref subst proveHyp nil 103 ref 496 remove 1041 remove appTerm nil cons cons 104 ref 1054 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp nil "p" 494 remove var 1065 remove cons nil cons nil cons cons 594 remove 900 ref subst subst eqMp eqMp nil 103 ref 214 ref 1052 ref appTerm nil cons cons 104 ref 1053 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 339 ref 337 ref 1052 remove nil cons cons 924 ref cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 1051 remove nil cons cons 104 ref 1050 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 347 remove 345 ref 1049 remove nil cons cons 925 ref cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 1048 remove nil cons cons 104 ref 1047 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 339 ref 337 ref 1046 remove nil cons cons 926 ref cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 1045 remove nil cons cons 104 ref 1044 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 339 ref 337 ref 1043 remove nil cons cons 927 ref cons nil cons cons 185 ref subst eqMp eqMp appThm appThm 625 remove appThm sym nil 103 ref 14 ref 462 ref appTerm 1066 def 474 ref appTerm 1067 def nil cons 1068 def cons 104 ref 444 ref 453 ref 518 remove appTerm 591 ref 536 remove appTerm 1069 def appTerm 460 ref appTerm appTerm 624 remove appTerm nil cons 1070 def cons nil cons 1071 def cons nil cons cons 1072 def 121 ref subst 1072 remove 178 ref subst 14 ref "_31812" 1 ref var 1073 def 444 ref 453 ref 35 ref 1073 remove varTerm 1074 def appTerm appTerm 1069 ref appTerm 460 ref appTerm appTerm 453 ref 1074 remove appTerm 460 ref appTerm 623 ref appTerm appTerm absTerm 1075 def 462 ref appTerm 1076 def appTerm refl 1077 def 1075 ref 474 ref appTerm betaConv appThm 145 ref 1076 remove betaConv appThm 1078 def 444 ref 453 ref 35 ref 474 ref appTerm 1079 def appTerm 1080 def 1069 ref appTerm 460 ref appTerm appTerm 453 ref 474 ref appTerm 1081 def 460 ref appTerm 623 ref appTerm appTerm refl appThm trans 1075 remove refl 1082 def 1067 remove assume appThm eqMp sym 615 ref 626 ref nil 14 ref 1079 ref appTerm 18 ref appTerm axiom 1083 def appThm 1084 def 1069 ref refl 1085 def appThm 460 ref refl 1086 def appThm nil "t2" 10 ref var 1087 def 692 ref cons "t1" 10 ref var 1088 def 1069 ref nil cons cons nil cons cons nil cons cons 1089 def 348 ref "t2" 43 ref var 1090 def 1008 ref 33 remove 0 ref 1 ref 0 ref 43 ref 560 remove nil cons cons opType nil cons cons opType constTerm 1091 def 18 ref appTerm "t1" 43 ref var 1092 def varTerm 1093 def appTerm 1090 ref varTerm 1094 def appTerm appTerm 1093 ref appTerm absTerm 1095 def 1094 ref appTerm 1096 def betaConv 1092 ref 86 ref 1095 ref appTerm 1097 def absTerm 1098 def 1093 ref appTerm 1099 def betaConv nil 86 ref 1098 ref appTerm 1100 def axiom nil 103 ref 1100 remove nil cons cons 104 ref 1099 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 376 ref 169 ref 1098 remove nil cons cons 173 ref 1093 ref nil cons cons nil cons 1101 def cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 1097 remove nil cons cons 104 ref 1096 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 376 ref 169 ref 1095 remove nil cons cons 173 ref 1094 ref nil cons cons nil cons 1102 def cons nil cons cons 185 ref subst eqMp eqMp 1103 def subst 1104 def subst trans appThm nil 1087 ref 623 ref nil cons cons 1088 ref 692 remove cons nil cons cons nil cons cons 1105 def 348 ref 1090 remove 1008 ref 1091 ref 474 ref appTerm 1093 ref appTerm 1094 ref appTerm appTerm 1094 ref appTerm absTerm 1106 def 1094 remove appTerm 1107 def betaConv 1092 remove 86 ref 1106 ref appTerm 1108 def absTerm 1109 def 1093 remove appTerm 1110 def betaConv nil 86 ref 1109 ref appTerm 1111 def axiom nil 103 ref 1111 remove nil cons cons 104 ref 1110 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 376 ref 169 ref 1109 remove nil cons cons 1101 remove cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 1108 remove nil cons cons 104 ref 1107 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 376 ref 169 ref 1106 remove nil cons cons 1102 remove cons nil cons cons 185 ref subst eqMp eqMp 1112 def subst 1113 def subst appThm sym nil 497 remove 591 remove nil cons cons 1114 def 501 remove 533 remove nil cons cons 1114 remove "y" 491 remove var 535 remove nil cons cons 68 ref 465 remove nil cons cons nil cons cons cons cons cons nil cons cons 558 remove "y" 43 ref var 1115 def 82 remove 570 ref 1091 remove 68 ref varTerm 1116 def appTerm 174 ref appTerm 1115 remove varTerm 1117 def appTerm appTerm appTerm 572 remove 1116 ref appTerm 571 ref appTerm 570 ref 1117 ref appTerm appTerm appTerm absTerm 1118 def 1117 ref appTerm 1119 def betaConv 173 ref 86 ref 1118 ref appTerm 1120 def absTerm 1121 def 174 ref appTerm 1122 def betaConv 569 ref 86 ref 1121 ref appTerm 1123 def absTerm 1124 def 570 ref appTerm 1125 def betaConv 68 ref 566 remove 1124 ref appTerm 1126 def absTerm 1127 def 1116 ref appTerm 1128 def betaConv nil 21 ref 1127 ref appTerm 1129 def axiom nil 103 ref 1129 remove nil cons cons 104 ref 1128 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 194 ref 195 ref 1127 remove nil cons cons 196 ref 1116 ref nil cons 1130 def cons nil cons 1131 def cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 1126 remove nil cons cons 104 ref 1125 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 770 remove 771 remove 1124 remove nil cons cons 772 remove 570 remove nil cons cons nil cons cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 1123 remove nil cons cons 104 ref 1122 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 376 ref 169 ref 1121 remove nil cons cons 378 remove cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 1120 remove nil cons cons 104 ref 1119 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 376 remove 169 remove 1118 remove nil cons cons 173 ref 1117 remove nil cons cons nil cons cons nil cons cons 185 ref subst eqMp eqMp subst subst eqMp eqMp eqMp nil 142 ref 1068 ref cons 143 ref 1070 ref cons nil cons 1132 def cons nil cons cons 157 ref subst deductAntisym eqMp nil 103 ref 1066 remove 18 ref appTerm 1133 def nil cons 1134 def cons 1071 remove cons nil cons cons 1135 def 121 ref subst 1135 remove 178 ref subst 1077 remove "_31810" 1 ref var 1136 def 444 ref 453 ref 35 ref 1136 remove varTerm 1137 def appTerm appTerm 1069 ref appTerm 460 ref appTerm appTerm 453 ref 1137 remove appTerm 460 ref appTerm 623 ref appTerm appTerm absTerm 18 ref appTerm betaConv appThm 1078 remove 444 ref 453 ref 35 ref 18 ref appTerm 1138 def appTerm 1139 def 1069 remove appTerm 460 ref appTerm appTerm 453 ref 18 ref appTerm 1140 def 460 ref appTerm 623 remove appTerm appTerm refl appThm trans 1082 remove 1133 remove assume appThm eqMp sym 615 ref 626 ref nil 14 ref 1138 ref appTerm 474 ref appTerm axiom 1141 def appThm 1142 def 1085 remove appThm 1086 remove appThm 1089 remove 1113 ref subst trans appThm 1105 remove 1104 ref subst appThm nil 925 remove nil cons cons 348 remove nil 8 ref 1008 remove 174 ref appTerm 174 ref appTerm nil cons cons nil cons nil cons cons 137 ref subst 184 remove eqMp 1143 def subst 1144 def subst trans sym 136 ref eqMp eqMp eqMp nil 142 ref 1134 remove cons 1145 def 1132 remove cons nil cons cons 157 ref subst deductAntisym eqMp 8 ref "Data.Bool.\\/" const 5 remove constTerm 1146 def 135 remove appTerm 134 remove 474 ref appTerm appTerm absTerm 1147 def 462 ref appTerm 1148 def betaConv nil 21 ref 1147 ref appTerm 1149 def axiom 1150 def nil 103 ref 1149 remove nil cons cons 1151 def 104 ref 1148 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 194 ref 195 ref 1147 ref nil cons cons 1152 def 196 ref 462 remove nil cons cons nil cons cons nil cons cons 185 ref subst eqMp eqMp nil 1145 remove 143 ref 1068 remove cons "R" 1 ref var 1153 def 1070 remove cons nil cons cons cons nil cons cons nil 103 ref 105 ref 148 ref appTerm 1154 def 1153 ref varTerm 1155 def appTerm 1156 def nil cons cons 104 ref 1155 ref nil cons 1157 def cons nil cons cons nil cons cons 165 ref subst nil 103 ref 105 ref 146 ref appTerm 1158 def 1155 ref appTerm nil cons cons 104 ref 105 ref 1156 remove appTerm 1155 ref appTerm nil cons cons nil cons cons nil cons cons 165 ref subst "r" 1 ref var 1159 def 105 ref 1158 remove 1159 ref varTerm 1160 def appTerm appTerm 1161 def 105 ref 1154 remove 1160 ref appTerm appTerm 1160 ref appTerm appTerm absTerm 1162 def 1155 remove appTerm 1163 def betaConv 14 ref 1146 ref 146 ref appTerm 1164 def 148 ref appTerm 1165 def appTerm refl 104 ref 21 ref 1159 ref 1161 remove 105 ref 782 remove 1160 ref appTerm appTerm 1160 ref appTerm 1166 def appTerm absTerm appTerm absTerm 148 remove appTerm betaConv appThm 128 remove 1164 remove appTerm refl 103 ref 104 ref 21 ref 1159 remove 105 ref 107 remove 1160 remove appTerm appTerm 1166 remove appTerm absTerm appTerm absTerm absTerm 1167 def 146 remove appTerm betaConv appThm nil 118 remove 1146 remove appTerm 1167 remove appTerm axiom 155 remove appThm eqMp 151 remove appThm eqMp 1165 remove assume eqMp nil 103 ref 21 ref 1162 ref appTerm nil cons cons 104 ref 1163 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 194 ref 195 ref 1162 remove nil cons cons 196 ref 1157 remove cons nil cons cons nil cons cons 185 ref subst eqMp eqMp eqMp eqMp 1168 def subst proveHyp proveHyp proveHyp eqMp eqMp eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp 482 remove "P" 479 remove var 477 remove nil cons cons "x" 456 ref var 604 remove nil cons cons nil cons cons nil cons cons 382 ref subst proveHyp eqMp nil 142 ref 598 remove cons 143 ref 588 remove cons nil cons 1169 def cons nil cons cons 157 ref subst deductAntisym eqMp eqMp eqMp nil 142 ref 595 remove cons 1169 ref cons nil cons cons 157 ref subst deductAntisym eqMp eqMp absThm eqMp nil 103 ref 547 remove 583 ref 105 ref 585 ref 583 remove varTerm appTerm appTerm 587 ref appTerm absTerm appTerm nil cons cons 104 ref 105 ref 586 remove appTerm 587 remove appTerm nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 581 remove 582 remove 585 remove nil cons cons 1169 remove cons nil cons cons 409 ref subst eqMp eqMp eqMp eqMp defineConstList 1170 def pop hdTl pop 456 remove constTerm 1171 def 17 remove appTerm 219 ref appTerm 1172 def 248 ref appTerm 1173 def 249 ref appTerm 1174 def appTerm 1175 def 452 ref 254 ref appTerm 248 ref appTerm appTerm absTerm 259 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 1176 def refl 1177 def 13 ref 0 ref 449 ref 0 ref 449 ref 2 ref cons opType 1178 def nil cons cons opType constTerm 451 ref appTerm 39 ref 0 ref 1178 ref 455 ref cons opType constTerm 1179 def 1176 ref appTerm appTerm assume sym appThm 1176 ref 451 remove appTerm betaConv trans "A" 455 remove cons nil cons 42 ref cons 55 ref subst 1177 remove appThm "p" 1178 ref var 1180 def 1180 remove varTerm 1181 def 1179 remove 1181 remove appTerm appTerm absTerm 1176 remove appTerm betaConv trans 145 ref 427 ref 215 ref 48 ref 0 ref 0 ref 447 ref 2 ref cons opType 1182 def 2 ref cons opType constTerm 1183 def refl "find" 447 ref var 1184 def 215 ref 1184 ref 214 ref 245 ref 214 ref 246 ref 444 ref 1184 remove varTerm 1185 def 248 ref appTerm 249 ref appTerm appTerm 251 ref 1175 ref 1185 ref 254 ref appTerm 248 ref appTerm appTerm absTerm 259 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm 1186 def absTerm 1187 def 219 ref appTerm betaConv 1188 def 1185 ref refl appThm 1186 ref 1185 remove appTerm betaConv trans absThm appThm absThm appThm appThm 48 ref 0 ref 1178 remove 2 ref cons opType constTerm refl 450 remove 427 remove 215 ref 1188 remove 452 ref refl appThm 1186 ref 452 remove appTerm betaConv trans absThm appThm absThm appThm appThm nil "r" 0 ref 201 ref 1182 ref nil cons cons opType var 1187 remove nil cons cons nil cons nil cons cons "B" 448 ref cons 339 ref cons 42 ref cons "r" 0 ref 43 remove 81 remove cons opType 1189 def var 1190 def 14 ref 86 ref 173 ref 48 ref 100 remove constTerm 1191 def "y" 73 remove var 1192 def 1190 remove varTerm 1193 def 174 remove appTerm 1194 def 1192 remove varTerm appTerm absTerm appTerm absTerm appTerm appTerm 568 remove 569 remove 86 remove 173 remove 1194 remove 571 remove appTerm absTerm appTerm absTerm appTerm appTerm absTerm 1195 def 1193 ref appTerm 1196 def betaConv nil 19 ref 0 ref 0 ref 1189 ref 2 ref cons opType 1197 def 2 ref cons opType constTerm 1195 ref appTerm 1198 def axiom nil 103 ref 1198 remove nil cons cons 104 ref 1196 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp "A" 1189 ref nil cons cons nil cons "P" 1197 remove var 1195 remove nil cons cons "x" 1189 remove var 1193 remove nil cons cons nil cons cons nil cons cons 185 ref subst eqMp eqMp subst subst eqMp nil 337 ref 215 ref 1183 remove 1186 ref appTerm 1199 def absTerm nil cons cons nil cons nil cons cons 341 ref subst 215 ref nil 8 ref 1199 ref nil cons 1200 def cons nil cons nil cons cons 137 ref subst "h" 0 ref 486 ref 27 remove cons opType 1201 def var 1202 def 48 ref 0 ref 0 ref 1201 ref 2 ref cons opType 1203 def 2 ref cons opType 1204 def constTerm 1205 def "f" 1201 ref var 1206 def 656 ref "x" 486 ref var 1207 def 444 ref 1206 ref varTerm 1208 def 1207 ref varTerm 1209 def appTerm appTerm 1210 def 453 ref 39 ref 0 ref 655 ref 658 ref cons opType constTerm 1211 def "f" 654 ref var 1212 def 214 ref 245 ref 214 ref 246 ref 14 ref 1212 remove varTerm 515 ref appTerm appTerm 35 ref 454 ref 259 ref appTerm 1213 def appTerm 1214 def appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1215 def 1209 ref appTerm appTerm 1216 def 1208 ref 39 ref 0 ref 0 ref 0 ref 486 ref 487 ref cons opType 1217 def 2 ref cons opType 1218 def 1217 ref nil cons 1219 def cons opType constTerm 1220 def "f" 1217 ref var 1221 def 214 ref 245 ref 214 ref 246 ref 659 ref 1221 remove varTerm 515 ref appTerm appTerm 514 ref 259 ref appTerm 248 ref appTerm 1222 def appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1223 def 1209 ref appTerm 1224 def appTerm appTerm 1225 def 1202 ref varTerm 1209 ref appTerm 1226 def appTerm appTerm absTerm appTerm absTerm appTerm absTerm 1227 def 39 ref 0 ref 1203 ref 1201 ref nil cons 1228 def cons opType constTerm 1229 def 1206 ref 214 ref 245 ref 214 ref 246 ref 444 ref 1208 ref 515 ref appTerm appTerm 1174 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1230 def appTerm 1231 def betaConv "g" 1217 ref var 1232 def 19 ref 1204 remove constTerm 1233 def 1202 ref 1205 ref 1206 ref 656 ref 1207 ref 1210 ref 1216 ref 1208 remove 1232 ref varTerm 1209 ref appTerm appTerm 1234 def appTerm 1226 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 1235 def 1223 ref appTerm 1236 def betaConv "p" 654 ref var 1237 def 19 ref 0 ref 1218 ref 2 ref cons opType 1238 def constTerm 1239 def 1232 remove 1233 ref 1202 remove 1205 ref 1206 ref 656 ref 1207 ref 1210 ref 453 ref 1237 remove varTerm 1209 ref appTerm appTerm 1234 remove appTerm 1226 remove appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 1240 def 1215 ref appTerm 1241 def betaConv "A" 487 remove cons 1242 def 557 remove cons 42 ref cons 573 ref subst nil 103 ref 19 ref 0 ref 655 ref 2 ref cons opType 1243 def constTerm 1240 ref appTerm nil cons cons 104 ref 1241 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp "A" 658 remove cons nil cons 1244 def "P" 655 ref var 1245 def 1240 remove nil cons cons "x" 654 ref var 1246 def 1215 remove nil cons cons nil cons cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 1239 remove 1235 ref appTerm nil cons cons 104 ref 1236 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp "A" 1219 remove cons nil cons 1247 def "P" 1218 ref var 1248 def 1235 remove nil cons cons "x" 1217 ref var 1249 def 1223 remove nil cons cons nil cons cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 1233 ref 1227 ref appTerm nil cons cons 104 ref 1231 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp "A" 1228 remove cons nil cons 1250 def "P" 1203 ref var 1251 def 1227 remove nil cons cons "x" 1201 ref var 1252 def 1230 ref nil cons cons nil cons cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 1205 ref 1206 remove 656 ref 1207 ref 1210 remove 1225 remove 1230 remove 1209 ref appTerm 1253 def appTerm appTerm absTerm appTerm absTerm 1254 def appTerm 1255 def nil cons cons 104 ref 1200 ref cons nil cons 1256 def cons nil cons cons 165 ref subst proveHyp nil 1251 ref "find" 1201 ref var 1257 def 105 ref 1254 ref 1257 ref varTerm 1258 def appTerm 1259 def appTerm 1199 ref appTerm 1260 def absTerm nil cons cons nil cons nil cons cons 1250 ref 42 ref cons 1261 def 327 ref subst subst 1257 remove nil 8 ref 1260 remove nil cons cons nil cons nil cons cons 137 ref subst nil 103 ref 1259 ref nil cons 1262 def cons 1256 ref cons nil cons cons 1263 def 121 ref subst 1263 remove 178 ref subst 1259 ref betaConv 1259 remove assume eqMp nil 103 ref 656 remove 1207 ref 444 ref 1258 ref 1209 ref appTerm appTerm 1216 remove 1258 ref 1224 remove appTerm appTerm 1253 remove appTerm appTerm absTerm 1264 def appTerm nil cons 1265 def cons 1266 def 1256 remove cons nil cons cons 1267 def 165 ref subst proveHyp 1267 ref 121 ref subst 1267 remove 178 ref subst 1186 ref 245 ref 246 ref 1258 ref 515 ref appTerm absTerm 1268 def absTerm 1269 def appTerm betaConv sym nil 337 ref 245 ref 214 ref 246 ref 444 ref 1269 ref 248 ref appTerm 1270 def 249 ref appTerm appTerm 251 ref 1175 ref 1269 ref 254 ref appTerm 1271 def 248 ref appTerm appTerm absTerm 259 ref appTerm appTerm 1272 def absTerm 1273 def appTerm 1274 def absTerm nil cons cons nil cons nil cons cons 341 ref subst 245 ref nil 8 ref 1274 remove nil cons cons nil cons nil cons cons 137 ref subst nil 337 ref 1273 remove nil cons cons nil cons nil cons cons 341 ref subst 246 ref nil 8 ref 1272 remove nil cons cons nil cons nil cons cons 137 ref subst 615 ref 1270 remove betaConv 343 ref appThm 1268 remove 249 ref appTerm betaConv trans appThm 251 ref 1175 ref refl 1271 remove betaConv 342 ref appThm 246 ref 1258 ref 514 ref 254 ref appTerm 1275 def 249 ref appTerm appTerm absTerm 248 ref appTerm betaConv trans appThm absThm 435 ref appThm appThm sym 615 ref nil 1207 ref 908 remove cons nil cons nil cons cons 1264 ref 1209 ref appTerm 1276 def betaConv nil 1266 remove 104 ref 1276 remove nil cons cons nil cons cons nil cons cons 165 ref subst 1242 remove nil cons "P" 654 ref var 1264 remove nil cons cons 1207 remove 1209 remove nil cons cons nil cons cons nil cons cons 185 ref subst eqMp eqMp subst appThm 251 ref 1175 ref 1258 ref 1275 remove 248 ref appTerm appTerm appTerm absTerm 259 ref appTerm 1277 def refl appThm sym 615 ref 626 remove 246 ref 14 ref 1211 remove "_31824" 654 remove var 1278 def 214 ref 245 ref 214 ref 246 ref 14 ref 1278 remove varTerm 515 ref appTerm appTerm 1214 ref appTerm absTerm appTerm absTerm appTerm absTerm 1279 def appTerm 1280 def 515 ref appTerm appTerm 1214 ref appTerm absTerm 1281 def 249 ref appTerm 1282 def betaConv 245 ref 214 ref 1281 ref appTerm 1283 def absTerm 1284 def 248 ref appTerm 1285 def betaConv 1279 ref 1280 remove appTerm 1286 def betaConv 1279 ref "_31822" 486 ref var 1287 def 35 ref 454 ref 218 ref 944 ref 1287 remove varTerm 1288 def appTerm appTerm 651 ref 1288 remove appTerm appTerm appTerm appTerm absTerm 1289 def appTerm betaConv sym nil 337 ref 245 ref 214 ref 246 ref 14 ref 1289 ref 515 ref appTerm 1290 def appTerm 1214 ref appTerm 1291 def absTerm 1292 def appTerm 1293 def absTerm nil cons cons nil cons nil cons cons 341 ref subst 245 ref nil 8 ref 1293 remove nil cons cons nil cons nil cons cons 137 ref subst nil 337 ref 1292 remove nil cons cons nil cons nil cons cons 341 ref subst 246 ref nil 8 ref 1291 remove nil cons cons nil cons nil cons cons 137 ref subst 1290 remove betaConv 14 ref "_31819" 201 ref var 1294 def 35 ref 454 ref 258 ref 1294 ref varTerm 1295 def appTerm appTerm appTerm absTerm 249 ref appTerm 1296 def appTerm refl 1294 ref 35 ref 454 ref 218 ref 944 ref 515 ref appTerm 1297 def appTerm 1298 def 1295 ref appTerm appTerm appTerm absTerm 1299 def 651 ref 515 ref appTerm 1300 def appTerm betaConv appThm 145 ref 1296 remove betaConv appThm 35 ref 454 ref 1298 ref 1300 ref appTerm 1301 def appTerm appTerm refl appThm trans 13 ref 0 ref 207 remove 213 remove nil cons cons opType constTerm 1302 def "_31818" 201 ref var 1303 def 1294 remove 35 ref 454 remove 218 ref 1303 remove varTerm appTerm 1295 remove appTerm appTerm appTerm absTerm absTerm 1304 def 248 ref appTerm 1305 def appTerm refl 1304 ref 1297 ref appTerm betaConv appThm 1302 remove refl 1305 remove betaConv appThm 1299 remove refl appThm trans 1304 remove refl 1038 ref appThm eqMp 920 ref appThm eqMp sym trans eqMp absThm eqMp eqMp absThm eqMp eqMp 1244 ref 1245 remove 1279 ref nil cons 1306 def cons 1246 remove 1289 remove nil cons cons nil cons cons nil cons cons 382 ref subst proveHyp nil 103 ref 48 ref 1243 remove constTerm 1279 remove appTerm nil cons cons 104 ref 1286 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp nil "p" 655 remove var 1306 remove cons nil cons nil cons cons 1244 remove 42 ref cons 900 ref subst subst eqMp eqMp nil 103 ref 214 ref 1284 ref appTerm nil cons cons 104 ref 1285 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 339 ref 337 ref 1284 remove nil cons cons 924 ref cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 1283 remove nil cons cons 104 ref 1282 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 339 ref 337 ref 1281 remove nil cons cons 927 ref cons nil cons cons 185 ref subst eqMp eqMp appThm 1258 ref refl 246 ref 659 ref 1220 remove "_31836" 1217 remove var 1307 def 214 ref 245 ref 214 ref 246 ref 659 ref 1307 remove varTerm 515 ref appTerm appTerm 1222 ref appTerm absTerm appTerm absTerm appTerm absTerm 1308 def appTerm 1309 def 515 ref appTerm appTerm 1222 ref appTerm absTerm 1310 def 249 ref appTerm 1311 def betaConv 245 ref 214 ref 1310 ref appTerm 1312 def absTerm 1313 def 248 ref appTerm 1314 def betaConv 1308 ref 1309 remove appTerm 1315 def betaConv 1308 ref "_31834" 486 ref var 1316 def 514 ref 218 ref 944 ref 1316 remove varTerm 1317 def appTerm 1318 def appTerm 651 ref 1317 remove appTerm appTerm appTerm 1318 remove appTerm absTerm 1319 def appTerm betaConv sym nil 337 ref 245 ref 214 ref 246 ref 659 ref 1319 ref 515 ref appTerm 1320 def appTerm 1222 ref appTerm 1321 def absTerm 1322 def appTerm 1323 def absTerm nil cons cons nil cons nil cons cons 341 ref subst 245 ref nil 8 ref 1323 remove nil cons cons nil cons nil cons cons 137 ref subst nil 337 ref 1322 remove nil cons cons nil cons nil cons cons 341 ref subst 246 ref nil 8 ref 1321 remove nil cons cons nil cons nil cons cons 137 ref subst 1320 remove betaConv 659 ref "_31831" 201 ref var 1324 def 514 ref 258 ref 1324 ref varTerm 1325 def appTerm appTerm 248 ref appTerm absTerm 249 ref appTerm 1326 def appTerm refl 1324 ref 514 ref 1298 remove 1325 ref appTerm appTerm 1297 ref appTerm absTerm 1327 def 1300 ref appTerm betaConv appThm 659 remove refl 1326 remove betaConv appThm 514 ref 1301 remove appTerm 1297 ref appTerm refl appThm trans 13 ref 0 ref 513 ref 0 ref 513 remove 2 ref cons opType nil cons cons opType constTerm 1328 def "_31830" 201 ref var 1329 def 1324 remove 514 remove 218 ref 1329 remove varTerm 1330 def appTerm 1325 remove appTerm appTerm 1330 remove appTerm absTerm absTerm 1331 def 248 ref appTerm 1332 def appTerm refl 1331 ref 1297 ref appTerm betaConv appThm 1328 remove refl 1332 remove betaConv appThm 1327 remove refl appThm trans 1331 remove refl 1038 ref appThm eqMp 920 ref appThm eqMp sym trans eqMp absThm eqMp eqMp absThm eqMp eqMp 1247 ref 1248 remove 1308 ref nil cons 1333 def cons 1249 remove 1319 remove nil cons cons nil cons cons nil cons cons 382 ref subst proveHyp nil 103 ref 48 ref 1238 remove constTerm 1308 remove appTerm nil cons cons 104 ref 1315 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp nil "p" 1218 remove var 1333 remove cons nil cons nil cons cons 1247 remove 42 ref cons 900 ref subst subst eqMp eqMp nil 103 ref 214 ref 1313 ref appTerm nil cons cons 104 ref 1314 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 339 ref 337 ref 1313 remove nil cons cons 924 ref cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 1312 remove nil cons cons 104 ref 1311 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 339 ref 337 ref 1310 remove nil cons cons 927 ref cons nil cons cons 185 ref subst eqMp eqMp appThm appThm 246 ref 444 ref 1229 remove "_31848" 1201 remove var 1334 def 214 ref 245 ref 214 ref 246 ref 444 ref 1334 remove varTerm 515 ref appTerm appTerm 1174 ref appTerm absTerm appTerm absTerm appTerm absTerm 1335 def appTerm 1336 def 515 ref appTerm appTerm 1174 ref appTerm absTerm 1337 def 249 ref appTerm 1338 def betaConv 245 ref 214 ref 1337 ref appTerm 1339 def absTerm 1340 def 248 ref appTerm 1341 def betaConv 1335 ref 1336 remove appTerm 1342 def betaConv 1335 ref "_31846" 486 remove var 1343 def 1172 ref 944 remove 1343 remove varTerm 1344 def appTerm appTerm 651 remove 1344 remove appTerm appTerm absTerm 1345 def appTerm betaConv sym nil 337 ref 245 ref 214 ref 246 ref 444 ref 1345 ref 515 remove appTerm 1346 def appTerm 1174 ref appTerm 1347 def absTerm 1348 def appTerm 1349 def absTerm nil cons cons nil cons nil cons cons 341 ref subst 245 ref nil 8 ref 1349 remove nil cons cons nil cons nil cons cons 137 ref subst nil 337 ref 1348 remove nil cons cons nil cons nil cons cons 341 ref subst 246 ref nil 8 ref 1347 remove nil cons cons nil cons nil cons cons 137 ref subst 1346 remove betaConv 444 ref "_31843" 201 ref var 1350 def 1173 remove 1350 ref varTerm 1351 def appTerm absTerm 249 ref appTerm 1352 def appTerm refl 1350 ref 1172 ref 1297 ref appTerm 1353 def 1351 ref appTerm absTerm 1354 def 1300 ref appTerm betaConv appThm 615 ref 1352 remove betaConv appThm 1353 remove 1300 remove appTerm refl appThm trans 13 ref 0 ref 446 ref 0 ref 446 ref 2 ref cons opType nil cons cons opType constTerm 1355 def "_31842" 201 ref var 1356 def 1350 remove 1172 remove 1356 remove varTerm appTerm 1351 remove appTerm absTerm absTerm 1357 def 248 ref appTerm 1358 def appTerm refl 1357 ref 1297 remove appTerm betaConv appThm 1355 remove refl 1358 remove betaConv appThm 1354 remove refl appThm trans 1357 remove refl 1038 remove appThm eqMp 920 remove appThm eqMp sym trans eqMp absThm eqMp eqMp absThm eqMp eqMp 1250 ref 1251 ref 1335 ref nil cons 1359 def cons 1252 ref 1345 remove nil cons cons nil cons cons nil cons cons 382 ref subst proveHyp nil 103 ref 1205 remove 1335 remove appTerm nil cons cons 104 ref 1342 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp nil "p" 1203 remove var 1359 remove cons nil cons nil cons cons 1261 remove 900 ref subst subst eqMp eqMp nil 103 ref 214 ref 1340 ref appTerm nil cons cons 104 ref 1341 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 339 ref 337 ref 1340 remove nil cons cons 924 ref cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 1339 remove nil cons cons 104 ref 1338 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 339 ref 337 ref 1337 remove nil cons cons 927 ref cons nil cons cons 185 ref subst eqMp eqMp appThm appThm 1277 remove betaConv appThm sym nil 103 ref 14 ref 1213 ref appTerm 1360 def 474 ref appTerm 1361 def nil cons 1362 def cons 104 ref 444 ref 453 ref 1214 remove appTerm 1258 remove 1222 remove appTerm 1363 def appTerm 1174 ref appTerm appTerm 453 ref 1213 ref appTerm 1174 ref appTerm 1363 ref appTerm appTerm nil cons 1364 def cons nil cons 1365 def cons nil cons cons 1366 def 121 ref subst 1366 remove 178 ref subst 14 ref "_31852" 1 ref var 1367 def 444 ref 453 ref 35 ref 1367 remove varTerm 1368 def appTerm appTerm 1363 ref appTerm 1174 ref appTerm appTerm 453 ref 1368 remove appTerm 1174 ref appTerm 1363 ref appTerm appTerm absTerm 1369 def 1213 ref appTerm 1370 def appTerm refl 1371 def 1369 ref 474 ref appTerm betaConv appThm 145 ref 1370 remove betaConv appThm 1372 def 444 ref 1080 remove 1363 ref appTerm 1174 ref appTerm appTerm 1081 remove 1174 ref appTerm 1363 ref appTerm appTerm refl appThm trans 1369 remove refl 1373 def 1361 remove assume appThm eqMp sym 615 ref 1084 remove 1363 ref refl 1374 def appThm 1174 ref refl 1375 def appThm nil 1087 ref 1174 ref nil cons 1376 def cons 1088 ref 1363 ref nil cons 1377 def cons nil cons cons nil cons cons 1378 def 1104 ref subst trans appThm nil 1087 remove 1377 ref cons 1088 remove 1376 ref cons nil cons cons nil cons cons 1379 def 1113 ref subst appThm nil 352 ref 1377 remove cons nil cons nil cons cons 1144 ref subst trans sym 136 ref eqMp eqMp eqMp nil 142 ref 1362 ref cons 143 ref 1364 ref cons nil cons 1380 def cons nil cons cons 157 ref subst deductAntisym eqMp nil 103 ref 1360 remove 18 ref appTerm 1381 def nil cons 1382 def cons 1365 remove cons nil cons cons 1383 def 121 ref subst 1383 remove 178 ref subst 1371 remove "_31850" 1 ref var 1384 def 444 ref 453 ref 35 ref 1384 remove varTerm 1385 def appTerm appTerm 1363 ref appTerm 1174 ref appTerm appTerm 453 remove 1385 remove appTerm 1174 ref appTerm 1363 ref appTerm appTerm absTerm 18 ref appTerm betaConv appThm 1372 remove 444 ref 1139 remove 1363 ref appTerm 1174 ref appTerm appTerm 1140 remove 1174 remove appTerm 1363 remove appTerm appTerm refl appThm trans 1373 remove 1381 remove assume appThm eqMp sym 615 remove 1142 remove 1374 remove appThm 1375 remove appThm 1378 remove 1113 remove subst trans appThm 1379 remove 1104 remove subst appThm nil 352 remove 1376 remove cons nil cons nil cons cons 1144 remove subst trans sym 136 ref eqMp eqMp eqMp nil 142 ref 1382 remove cons 1386 def 1380 remove cons nil cons cons 157 ref subst deductAntisym eqMp 1147 ref 1213 ref appTerm 1387 def betaConv 1150 ref nil 1151 ref 104 ref 1387 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 194 ref 1152 ref 196 ref 1213 remove nil cons cons nil cons cons nil cons cons 185 ref subst eqMp eqMp nil 1386 remove 143 ref 1362 remove cons 1153 ref 1364 remove cons nil cons cons cons nil cons cons 1168 ref subst proveHyp proveHyp proveHyp eqMp eqMp eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp "A" 448 remove cons nil cons "P" 1182 remove var 1186 remove nil cons cons "x" 447 remove var 1269 remove nil cons cons nil cons cons nil cons cons 382 ref subst proveHyp eqMp nil 142 ref 1265 remove cons 143 ref 1200 remove cons nil cons 1388 def cons nil cons cons 157 ref subst deductAntisym eqMp eqMp eqMp nil 142 ref 1262 remove cons 1388 ref cons nil cons cons 157 ref subst deductAntisym eqMp eqMp absThm eqMp nil 103 ref 1233 remove 1252 ref 105 ref 1254 ref 1252 remove varTerm appTerm appTerm 1199 ref appTerm absTerm appTerm nil cons cons 104 ref 105 ref 1255 remove appTerm 1199 remove appTerm nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 1250 remove 1251 remove 1254 remove nil cons cons 1388 remove cons nil cons cons 409 ref subst eqMp eqMp eqMp absThm eqMp eqMp eqMp eqMp defineConstList 1389 def pop hdTl pop 449 remove constTerm 1390 def 445 ref varTerm 1391 def appTerm 212 ref appTerm 211 ref appTerm 1392 def absTerm 1393 def defineConst 1394 def pop 446 remove constTerm 1395 def 219 ref appTerm appTerm 1390 remove 219 ref appTerm 1396 def 212 ref appTerm 211 ref appTerm appTerm absTerm 1397 def nil cons cons nil cons nil cons cons 341 ref subst 445 remove nil 8 ref 444 ref 1395 remove 1391 ref appTerm appTerm 1392 remove appTerm nil cons cons nil cons nil cons cons 137 ref subst 1394 remove 1391 ref refl appThm 1393 remove 1391 remove appTerm betaConv trans eqMp absThm eqMp nil 214 ref 1397 remove appTerm thm nil 345 remove 458 ref 209 ref "Number.Natural.Fibonacci.decode" "_31715" 10 remove var 1398 def 439 remove 212 ref appTerm 211 ref appTerm 1399 def 1398 ref varTerm 1400 def appTerm 1401 def absTerm 1402 def defineConst 1403 def pop 242 remove constTerm 1404 def 460 ref appTerm appTerm 1399 remove 460 ref appTerm appTerm absTerm 1405 def nil cons cons nil cons nil cons cons 349 remove subst 1398 remove nil 8 ref 209 ref 1404 remove 1400 ref appTerm appTerm 1401 remove appTerm nil cons cons nil cons nil cons cons 137 ref subst 1403 remove 1400 ref refl appThm 1402 remove 1400 remove appTerm betaConv trans eqMp absThm eqMp nil 24 ref 1405 remove appTerm thm nil "P" 0 ref "Probability.Random.random" typeOp nil opType 1406 def 2 ref cons opType 1407 def var 1408 def "r" 1406 ref var 1409 def 209 ref "Number.Natural.Fibonacci.random" "_32030" 1406 ref var 1410 def 469 ref "Number.Natural.Fibonacci.random.dest" "dest" 0 ref 1 ref 0 ref 201 ref 0 ref 201 ref 0 ref 201 ref 0 ref 1406 ref 202 ref cons opType 1411 def nil cons cons opType nil cons cons opType nil cons cons opType nil cons cons opType 1412 def var 1413 def nil cons cons nil cons 1413 ref 21 ref 68 ref 214 ref 215 ref 214 ref 245 ref 214 ref 246 ref 19 ref 0 ref 1407 ref 2 ref cons opType 1414 def constTerm 1415 def 1409 ref 209 ref 1413 remove varTerm 1416 def 1116 ref appTerm 219 ref appTerm 248 ref appTerm 249 ref appTerm 1409 ref varTerm 1417 def appTerm appTerm 39 ref 0 ref 0 ref 0 ref 485 ref 1406 ref 1406 ref nil cons 1418 def cons opType 1419 def 202 ref cons opType 1420 def 2 ref cons opType 1421 def 1420 ref nil cons 1422 def cons opType constTerm 1423 def "f" 1420 ref var 1424 def 1415 ref "r1" 1406 ref var 1425 def 1415 ref "r2" 1406 ref var 1426 def 209 ref 1424 ref varTerm 508 ref 0 ref 1406 ref 0 ref 1406 ref 1419 ref nil cons 1427 def cons opType 1428 def nil cons cons opType constTerm 1429 def 1425 ref varTerm 1430 def appTerm 1431 def 1426 ref varTerm 1432 def appTerm 1433 def appTerm appTerm 1434 def "b'" 1 ref var 1435 def 253 ref 6 ref 1435 ref varTerm 1436 def appTerm 1437 def 1116 ref appTerm 1438 def appTerm 219 ref appTerm 1439 def 251 ref 1416 ref 1436 ref appTerm 253 ref 1436 ref appTerm 1440 def 256 ref appTerm 219 ref appTerm 1441 def appTerm 254 ref appTerm 248 ref appTerm 1432 ref appTerm absTerm 259 ref appTerm appTerm absTerm "Probability.Random.bit" const 1407 ref constTerm 1442 def 1430 ref appTerm 1443 def appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm "Probability.Random.split" const 1428 remove constTerm 1444 def 1417 ref appTerm 1445 def appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 1446 def refl 1447 def 13 ref 0 ref 1412 ref 0 ref 1412 ref 2 ref cons opType 1448 def nil cons cons opType constTerm 1416 ref appTerm 39 ref 0 ref 1448 ref 1412 ref nil cons 1449 def cons opType constTerm 1450 def 1446 ref appTerm appTerm assume sym appThm 1446 ref 1416 remove appTerm betaConv trans "A" 1449 remove cons nil cons 1451 def 42 ref cons 55 remove subst 1447 remove appThm "p" 1448 ref var 1452 def 1452 remove varTerm 1453 def 1450 remove 1453 remove appTerm appTerm absTerm 1446 ref appTerm betaConv trans "h" 0 ref 485 ref 1 ref 485 ref 201 ref 485 ref 201 ref 485 remove 201 ref 1418 ref cons opType 1454 def nil cons 1455 def cons opType 1456 def nil cons 1457 def cons opType 1458 def nil cons 1459 def cons opType 1460 def 202 ref cons opType 1461 def var 1462 def 48 ref 0 ref 0 ref 1461 ref 2 ref cons opType 1463 def 2 ref cons opType 1464 def constTerm 1465 def "f" 1461 ref var 1466 def 19 ref 0 ref 0 ref 1460 ref 2 ref cons opType 1467 def 2 ref cons opType 1468 def constTerm 1469 def "x" 1460 ref var 1470 def 209 ref 1466 ref varTerm 1471 def 1470 ref varTerm 1472 def appTerm appTerm 1473 def 253 ref 39 ref 0 ref 1468 ref 1467 ref nil cons 1474 def cons opType constTerm 1475 def "f" 1467 ref var 1476 def 21 ref 68 ref 214 ref 245 ref 214 ref 215 ref 214 ref 246 ref 1415 ref 1409 ref 14 ref 1476 remove varTerm 508 ref 0 ref 1 ref 0 ref 1458 ref 1460 ref nil cons 1477 def cons opType nil cons cons opType constTerm 1478 def 1116 ref appTerm 508 ref 0 ref 201 ref 0 ref 1456 ref 1459 ref cons opType nil cons cons opType constTerm 1479 def 219 ref appTerm 508 ref 0 ref 201 ref 0 ref 1454 ref 1457 ref cons opType nil cons cons opType constTerm 1480 def 248 ref appTerm 508 remove 0 ref 201 ref 0 ref 1406 ref 1455 ref cons opType nil cons cons opType constTerm 1481 def 249 ref appTerm 1417 ref appTerm 1482 def appTerm 1483 def appTerm 1484 def appTerm 1485 def appTerm appTerm 39 ref 0 ref 0 ref 0 ref 1419 ref 2 ref cons opType 1486 def 2 ref cons opType 1487 def 1486 ref nil cons 1488 def cons opType constTerm 1489 def "f" 1486 ref var 1490 def 1415 ref 1425 ref 1415 ref 1426 ref 14 ref 1490 ref varTerm 1433 ref appTerm appTerm 1491 def 1435 ref 35 ref 1438 remove appTerm absTerm 1443 ref appTerm 1492 def appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1493 def 1445 ref appTerm 1494 def appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1495 def 1472 ref appTerm appTerm 1496 def 1471 ref 39 ref 0 ref 0 ref 0 ref 1460 ref 1477 ref cons opType 1497 def 2 ref cons opType 1498 def 1497 ref nil cons 1499 def cons opType constTerm 1500 def "f" 1497 ref var 1501 def 21 ref 68 ref 214 ref 245 ref 214 ref 215 ref 214 ref 246 ref 1415 ref 1409 ref 13 ref 0 ref 1460 ref 1474 ref cons opType constTerm 1502 def 1501 remove varTerm 1485 ref appTerm appTerm 39 ref 0 ref 0 ref 0 ref 1419 ref 1477 ref cons opType 1503 def 2 ref cons opType 1504 def 1503 ref nil cons 1505 def cons opType constTerm 1506 def "f" 1503 ref var 1507 def 1415 ref 1425 ref 1415 ref 1426 ref 1502 ref 1507 ref varTerm 1433 ref appTerm appTerm 1508 def 1435 ref 251 ref 1478 ref 1436 ref appTerm 1509 def 1479 ref 1441 ref appTerm 1510 def 1480 ref 254 ref appTerm 1511 def 1481 ref 248 ref appTerm 1512 def 1432 ref appTerm 1513 def appTerm 1514 def appTerm appTerm 1515 def absTerm 1516 def 259 ref appTerm absTerm 1443 ref appTerm 1517 def appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1518 def 1445 ref appTerm 1519 def appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1520 def 1472 ref appTerm 1521 def appTerm appTerm 1522 def 1462 ref varTerm 1472 ref appTerm 1523 def appTerm appTerm absTerm appTerm absTerm appTerm absTerm 1524 def 39 ref 0 ref 1463 ref 1461 ref nil cons 1525 def cons opType constTerm 1526 def 1466 ref 21 ref 68 ref 214 ref 245 ref 214 ref 215 ref 214 ref 246 ref 1415 ref 1409 ref 209 ref 1471 ref 1485 ref appTerm appTerm 219 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1527 def appTerm 1528 def betaConv "g" 1497 ref var 1529 def 19 ref 1464 remove constTerm 1530 def 1462 ref 1465 ref 1466 ref 1469 ref 1470 ref 1473 ref 1496 ref 1471 remove 1529 ref varTerm 1472 ref appTerm appTerm 1531 def appTerm 1523 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 1532 def 1520 ref appTerm 1533 def betaConv "p" 1467 ref var 1534 def 19 ref 0 ref 1498 ref 2 ref cons opType 1535 def constTerm 1536 def 1529 remove 1530 ref 1462 remove 1465 ref 1466 ref 1469 ref 1470 ref 1473 ref 253 ref 1534 remove varTerm 1472 ref appTerm appTerm 1531 remove appTerm 1523 remove appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 1537 def 1495 ref appTerm 1538 def betaConv "A" 1477 ref cons 1539 def 918 remove cons 42 ref cons 573 remove subst nil 103 ref 19 ref 0 ref 1468 ref 2 ref cons opType 1540 def constTerm 1537 ref appTerm nil cons cons 104 ref 1538 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp "A" 1474 remove cons nil cons 1541 def "P" 1468 ref var 1542 def 1537 remove nil cons cons "x" 1467 ref var 1543 def 1495 remove nil cons cons nil cons cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 1536 remove 1532 ref appTerm nil cons cons 104 ref 1533 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp "A" 1499 remove cons nil cons 1544 def "P" 1498 ref var 1545 def 1532 remove nil cons cons "x" 1497 ref var 1546 def 1520 remove nil cons cons nil cons cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 1530 ref 1524 ref appTerm nil cons cons 104 ref 1528 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp "A" 1525 remove cons nil cons 1547 def "P" 1463 ref var 1548 def 1524 remove nil cons cons "x" 1461 ref var 1549 def 1527 ref nil cons cons nil cons cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 1465 ref 1466 remove 1469 ref 1470 ref 1473 remove 1522 remove 1527 remove 1472 ref appTerm 1550 def appTerm appTerm absTerm appTerm absTerm 1551 def appTerm 1552 def nil cons cons 104 ref 48 ref 0 ref 1448 ref 2 ref cons opType constTerm 1446 ref appTerm 1553 def nil cons 1554 def cons nil cons 1555 def cons nil cons cons 165 ref subst proveHyp nil 1548 ref "dest" 1461 ref var 1556 def 105 ref 1551 ref 1556 ref varTerm 1557 def appTerm 1558 def appTerm 1553 ref appTerm 1559 def absTerm nil cons cons nil cons nil cons cons 1547 ref 42 ref cons 1560 def 327 ref subst subst 1556 remove nil 8 ref 1559 remove nil cons cons nil cons nil cons cons 137 ref subst nil 103 ref 1558 ref nil cons 1561 def cons 1555 ref cons nil cons cons 1562 def 121 ref subst 1562 remove 178 ref subst 1558 ref betaConv 1558 remove assume eqMp nil 103 ref 1469 remove 1470 ref 209 ref 1557 ref 1472 ref appTerm appTerm 1496 remove 1557 ref 1521 remove appTerm appTerm 1550 remove appTerm appTerm absTerm 1563 def appTerm nil cons 1564 def cons 1565 def 1555 remove cons nil cons cons 1566 def 165 ref subst proveHyp 1566 ref 121 ref subst 1566 remove 178 ref subst 1446 ref 68 ref 215 ref 245 ref 246 ref 1409 ref 1557 ref 1485 ref appTerm absTerm 1567 def absTerm 1568 def absTerm 1569 def absTerm 1570 def absTerm 1571 def appTerm betaConv sym nil 195 ref 68 ref 214 ref 215 ref 214 ref 245 ref 214 ref 246 ref 1415 ref 1409 ref 209 ref 1571 ref 1116 ref appTerm 1572 def 219 ref appTerm 248 ref appTerm 249 ref appTerm 1417 ref appTerm appTerm 1423 ref 1424 ref 1415 ref 1425 ref 1415 ref 1426 ref 1434 ref 1435 ref 1439 ref 251 ref 1571 ref 1436 ref appTerm 1573 def 1441 ref appTerm 254 ref appTerm 248 ref appTerm 1432 ref appTerm absTerm 259 ref appTerm appTerm absTerm 1443 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1445 ref appTerm appTerm 1574 def absTerm 1575 def appTerm 1576 def absTerm 1577 def appTerm 1578 def absTerm 1579 def appTerm 1580 def absTerm 1581 def appTerm 1582 def absTerm nil cons cons nil cons nil cons cons 344 ref subst 68 ref nil 8 ref 1582 remove nil cons cons nil cons nil cons cons 137 ref subst nil 337 ref 1581 remove nil cons cons nil cons nil cons cons 341 ref subst 215 ref nil 8 ref 1580 remove nil cons cons nil cons nil cons cons 137 ref subst nil 337 ref 1579 remove nil cons cons nil cons nil cons cons 341 ref subst 245 ref nil 8 ref 1578 remove nil cons cons nil cons nil cons cons 137 ref subst nil 337 ref 1577 remove nil cons cons nil cons nil cons cons 341 ref subst 246 ref nil 8 ref 1576 remove nil cons cons nil cons nil cons cons 137 ref subst nil 1408 ref 1575 remove nil cons cons nil cons nil cons cons "A" 1418 ref cons 1583 def nil cons 1584 def 42 ref cons 327 ref subst 1585 def subst 1409 ref nil 8 ref 1574 remove nil cons cons nil cons nil cons cons 137 ref subst 428 ref 1572 remove betaConv 616 ref appThm 1570 remove 219 ref appTerm betaConv trans 342 ref appThm 1569 remove 248 ref appTerm betaConv trans 343 remove appThm 1568 remove 249 ref appTerm betaConv trans 1417 ref refl appThm 1567 remove 1417 ref appTerm betaConv trans appThm 1423 ref refl 1586 def 1424 ref 1415 ref refl 1587 def 1425 ref 1587 ref 1426 ref 1434 ref refl 1588 def 1435 ref 1439 ref refl 251 ref 1573 remove betaConv 1441 ref refl appThm 215 ref 245 ref 246 ref 1409 ref 1557 ref 1509 ref 1484 ref appTerm appTerm absTerm absTerm absTerm absTerm 1441 ref appTerm betaConv trans 433 remove appThm 245 ref 246 ref 1409 ref 1557 ref 1509 ref 1510 ref 1483 ref appTerm appTerm appTerm absTerm absTerm absTerm 254 ref appTerm betaConv trans 342 remove appThm 246 ref 1409 ref 1557 ref 1509 ref 1510 ref 1511 ref 1482 ref appTerm appTerm appTerm appTerm absTerm absTerm 248 ref appTerm betaConv trans 1432 ref refl appThm 1409 ref 1557 ref 1509 ref 1510 ref 1511 ref 1512 ref 1417 ref appTerm appTerm appTerm appTerm appTerm absTerm 1432 ref appTerm betaConv trans absThm 435 remove appThm appThm absThm 1443 ref refl appThm appThm absThm appThm absThm appThm absThm appThm 1445 ref refl 1589 def appThm appThm sym 428 ref nil 1470 ref 1485 ref nil cons cons nil cons nil cons cons 1563 ref 1472 ref appTerm 1590 def betaConv nil 1565 remove 104 ref 1590 remove nil cons cons nil cons cons nil cons cons 165 ref subst 1539 remove nil cons "P" 1467 ref var 1563 remove nil cons cons 1470 remove 1472 remove nil cons cons nil cons cons nil cons cons 185 ref subst eqMp eqMp subst appThm 1423 ref 1424 ref 1415 ref 1425 ref 1415 ref 1426 ref 1434 ref 1435 ref 1439 ref 251 ref 1557 ref 1515 remove appTerm absTerm 259 ref appTerm appTerm absTerm 1443 ref appTerm 1591 def appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1445 ref appTerm refl appThm sym 428 ref 253 ref refl 1592 def 1409 ref 14 ref 1475 ref "_31902" 1467 ref var 1593 def 21 ref 68 ref 214 ref 245 ref 214 ref 215 ref 214 ref 246 ref 1415 ref 1409 ref 14 ref 1593 remove varTerm 1485 ref appTerm appTerm 1494 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 1594 def appTerm 1595 def 1485 ref appTerm appTerm 1494 ref appTerm absTerm 1596 def 1417 ref appTerm 1597 def betaConv 246 ref 1415 ref 1596 ref appTerm 1598 def absTerm 1599 def 249 ref appTerm 1600 def betaConv 215 ref 214 ref 1599 ref appTerm 1601 def absTerm 1602 def 219 ref appTerm 1603 def betaConv 245 ref 214 ref 1602 ref appTerm 1604 def absTerm 1605 def 248 ref appTerm 1606 def betaConv 68 ref 214 ref 1605 ref appTerm 1607 def absTerm 1608 def 1116 ref appTerm 1609 def betaConv 1594 ref 1595 remove appTerm 1610 def betaConv 1594 ref "_31900" 1460 ref var 1611 def 1489 ref 1490 ref 1415 ref 1425 ref 1415 ref 1426 ref 1491 ref 1435 ref 35 ref 1437 ref 1475 remove "fn" 1467 remove var 1612 def 21 ref "a" 1 ref var 1613 def 19 ref 0 ref 0 ref 1458 ref 2 ref cons opType 1614 def 2 ref cons opType constTerm 1615 def "b" 1458 ref var 1616 def 14 ref 1612 remove varTerm 1478 ref 1613 ref varTerm 1617 def appTerm 1616 ref varTerm 1618 def appTerm 1619 def appTerm appTerm 1617 remove appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1620 def 1611 remove varTerm 1621 def appTerm appTerm appTerm absTerm 1443 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1444 ref 39 ref 0 ref 0 ref 0 ref 1454 ref 1418 ref cons opType 1622 def 2 ref cons opType 1622 ref nil cons cons opType constTerm "fn" 1622 remove var 1623 def 214 ref 646 ref 1415 ref "b" 1406 ref var 1624 def 13 ref 0 ref 1406 ref 1407 ref nil cons 1625 def cons opType constTerm 1626 def 1623 remove varTerm 1481 ref 648 ref appTerm 1624 ref varTerm 1627 def appTerm 1628 def appTerm appTerm 1627 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1629 def 39 ref 0 ref 0 ref 0 ref 1456 ref 1455 ref cons opType 1630 def 2 ref cons opType 1630 ref nil cons cons opType constTerm "fn" 1630 remove var 1631 def 214 ref 646 ref 19 ref 0 ref 0 ref 1454 ref 2 ref cons opType 1632 def 2 ref cons opType constTerm 1633 def "b" 1454 ref var 1634 def 13 ref 0 ref 1454 ref 1632 remove nil cons cons opType constTerm 1631 remove varTerm 1480 ref 648 ref appTerm 1634 ref varTerm 1635 def appTerm 1636 def appTerm appTerm 1635 remove appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1637 def 39 ref 0 ref 0 ref 0 ref 1458 ref 1457 ref cons opType 1638 def 2 ref cons opType 1638 ref nil cons cons opType constTerm "fn" 1638 remove var 1639 def 214 ref 646 ref 19 ref 0 ref 0 ref 1456 ref 2 ref cons opType 1640 def 2 ref cons opType constTerm 1641 def "b" 1456 ref var 1642 def 13 ref 0 ref 1456 ref 1640 remove nil cons cons opType constTerm 1639 remove varTerm 1479 ref 648 ref appTerm 1642 ref varTerm 1643 def appTerm 1644 def appTerm appTerm 1643 remove appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1645 def 39 ref 0 ref 0 ref 0 ref 1460 ref 1459 ref cons opType 1646 def 2 ref cons opType 1646 ref nil cons cons opType constTerm "fn" 1646 remove var 1647 def 21 ref 1613 ref 1615 remove 1616 ref 13 ref 0 ref 1458 ref 1614 remove nil cons cons opType constTerm 1647 remove varTerm 1619 remove appTerm appTerm 1618 remove appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1648 def 1621 remove appTerm appTerm appTerm appTerm appTerm appTerm absTerm 1649 def appTerm betaConv sym nil 195 ref 68 ref 214 ref 245 ref 214 ref 215 ref 214 ref 246 ref 1415 ref 1409 ref 14 ref 1649 ref 1485 ref appTerm 1650 def appTerm 1494 remove appTerm 1651 def absTerm 1652 def appTerm 1653 def absTerm 1654 def appTerm 1655 def absTerm 1656 def appTerm 1657 def absTerm 1658 def appTerm 1659 def absTerm nil cons cons nil cons nil cons cons 344 ref subst 68 ref nil 8 ref 1659 remove nil cons cons nil cons nil cons cons 137 ref subst nil 337 ref 1658 remove nil cons cons nil cons nil cons cons 341 ref subst 245 ref nil 8 ref 1657 remove nil cons cons nil cons nil cons cons 137 ref subst nil 337 ref 1656 remove nil cons cons nil cons nil cons cons 341 ref subst 215 ref nil 8 ref 1655 remove nil cons cons nil cons nil cons cons 137 ref subst nil 337 ref 1654 remove nil cons cons nil cons nil cons cons 341 ref subst 246 ref nil 8 ref 1653 remove nil cons cons nil cons nil cons cons 137 ref subst nil 1408 ref 1652 remove nil cons cons nil cons nil cons cons 1585 ref subst 1409 ref nil 8 ref 1651 remove nil cons cons nil cons nil cons cons 137 ref subst 1650 remove betaConv 14 ref "_31894" 1406 ref var 1660 def 1493 remove 1444 ref 1660 ref varTerm appTerm 1661 def appTerm absTerm 1662 def 1417 ref appTerm 1663 def appTerm refl 1660 ref 1489 ref 1490 ref 1415 ref 1425 ref 1415 ref 1426 ref 1491 ref 1435 ref 35 ref 1437 ref 1620 remove 1485 ref appTerm 1664 def appTerm appTerm absTerm 1443 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1665 def 1661 ref appTerm absTerm 1666 def 1629 ref 1637 ref 1645 ref 1648 ref 1485 ref appTerm 1667 def appTerm 1668 def appTerm 1669 def appTerm 1670 def appTerm betaConv appThm 145 ref 1663 remove betaConv appThm 1665 remove 1444 ref 1670 ref appTerm 1671 def appTerm refl appThm trans 13 ref 0 ref 1407 remove 1414 ref nil cons cons opType constTerm 1672 def "_31893" 201 ref var 1673 def 1662 remove absTerm 1674 def 249 ref appTerm 1675 def appTerm refl 1673 ref 1666 ref absTerm 1676 def 39 ref 0 ref 0 ref 0 ref 1454 ref 202 ref cons opType 1677 def 2 ref cons opType 1677 ref nil cons cons opType constTerm "fn" 1677 remove var 1678 def 214 ref 646 ref 1415 ref 1624 ref 209 ref 1678 remove varTerm 1628 remove appTerm appTerm 648 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1679 def 1669 remove appTerm 1680 def appTerm betaConv appThm 1672 ref refl 1681 def 1675 remove betaConv appThm 1666 remove refl appThm trans 13 ref 0 ref 0 ref 201 ref 1625 remove cons opType 1682 def 0 ref 1682 ref 2 ref cons opType nil cons cons opType constTerm 1683 def "_31892" 201 ref var 1684 def 1674 remove absTerm 1685 def 248 ref appTerm 1686 def appTerm refl 1684 ref 1676 ref absTerm 1687 def 39 ref 0 ref 0 ref 0 ref 1456 ref 202 ref cons opType 1688 def 2 ref cons opType 1688 ref nil cons cons opType constTerm "fn" 1688 remove var 1689 def 214 ref 646 ref 1633 remove 1634 ref 209 ref 1689 remove varTerm 1636 remove appTerm appTerm 648 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1690 def 1668 remove appTerm 1691 def appTerm betaConv appThm 1683 remove refl 1686 remove betaConv appThm 1676 remove refl appThm trans 13 ref 0 ref 0 ref 201 ref 1682 remove nil cons cons opType 1692 def 0 ref 1692 ref 2 ref cons opType nil cons cons opType constTerm 1693 def "_31891" 201 ref var 1694 def 1685 remove absTerm 219 ref appTerm 1695 def appTerm refl 1694 ref 1687 ref absTerm 1696 def 39 ref 0 ref 0 ref 0 ref 1458 ref 202 remove cons opType 1697 def 2 ref cons opType 1697 ref nil cons cons opType constTerm "fn" 1697 remove var 1698 def 214 ref 646 ref 1641 remove 1642 ref 209 ref 1698 remove varTerm 1644 remove appTerm appTerm 648 remove appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1699 def 1667 ref appTerm 1700 def appTerm betaConv appThm 1693 remove refl 1695 remove betaConv appThm 1687 remove refl appThm trans 13 ref 0 ref 0 ref 201 ref 1692 remove nil cons cons opType 1701 def 0 ref 1701 remove 2 ref cons opType nil cons cons opType constTerm 1702 def "_31890" 1 ref var 1703 def 1694 remove 1684 remove 1673 remove 1660 remove 1489 ref 1490 ref 1415 ref 1425 ref 1415 ref 1426 ref 1491 ref 1435 ref 35 ref 1437 remove 1703 remove varTerm appTerm appTerm absTerm 1443 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1661 remove appTerm absTerm absTerm absTerm absTerm absTerm 1704 def 1116 ref appTerm 1705 def appTerm refl 1704 ref 1664 remove appTerm betaConv appThm 1702 remove refl 1705 remove betaConv appThm 1696 remove refl appThm trans 1704 remove refl nil 1616 remove 1484 ref nil cons cons 1613 remove 1130 remove cons nil cons cons nil cons cons 1706 def 70 remove "B" 1459 remove cons nil cons cons 42 ref cons 1707 def 1025 ref subst subst appThm eqMp 1027 remove 209 ref "_31882" 1458 ref var 1708 def 1699 ref 1708 remove varTerm appTerm absTerm 1709 def 1484 ref appTerm 1710 def appTerm refl 1709 ref 1667 ref appTerm betaConv appThm 428 ref 1710 remove betaConv appThm 1700 ref refl appThm trans 1709 remove refl 1706 remove 1707 remove 902 ref subst subst 1711 def appThm eqMp appThm nil 1642 remove 1483 ref nil cons cons 910 remove cons nil cons cons 1712 def 338 ref "B" 1457 remove cons nil cons cons 42 ref cons 1713 def 1025 ref subst subst eqMp 1714 def appThm eqMp 1031 ref 209 ref "_31884" 1458 ref var 1715 def 1690 ref 1645 ref 1715 remove varTerm appTerm appTerm absTerm 1716 def 1484 ref appTerm 1717 def appTerm refl 1716 ref 1667 ref appTerm betaConv appThm 428 ref 1717 remove betaConv appThm 1691 ref refl appThm trans 1716 remove refl 1711 ref appThm eqMp appThm 1031 remove 209 ref "_31876" 1456 ref var 1718 def 1690 ref 1718 remove varTerm appTerm absTerm 1719 def 1483 ref appTerm 1720 def appTerm refl 1719 ref 1645 ref 1484 ref appTerm 1721 def appTerm betaConv appThm 428 ref 1720 remove betaConv appThm 1690 ref 1721 ref appTerm refl appThm trans 1719 remove refl 1712 remove 1713 remove 902 ref subst subst 1722 def appThm eqMp appThm nil 1634 remove 1482 ref nil cons cons 916 remove cons nil cons cons 1723 def 338 ref "B" 1455 remove cons nil cons cons 42 ref cons 1724 def 1025 ref subst subst eqMp eqMp 1725 def appThm eqMp 688 ref 209 ref "_31886" 1458 ref var 1726 def 1679 ref 1637 ref 1645 ref 1726 remove varTerm appTerm appTerm appTerm absTerm 1727 def 1484 ref appTerm 1728 def appTerm refl 1727 ref 1667 ref appTerm betaConv appThm 428 ref 1728 remove betaConv appThm 1680 ref refl appThm trans 1727 remove refl 1711 ref appThm eqMp appThm 688 ref 209 ref "_31878" 1456 ref var 1729 def 1679 ref 1637 ref 1729 remove varTerm appTerm appTerm absTerm 1730 def 1483 ref appTerm 1731 def appTerm refl 1730 ref 1721 ref appTerm betaConv appThm 428 ref 1731 remove betaConv appThm 1679 ref 1637 ref 1721 ref appTerm 1732 def appTerm refl appThm trans 1730 remove refl 1722 ref appThm eqMp appThm 688 remove 209 ref "_31872" 1454 ref var 1733 def 1679 ref 1733 remove varTerm appTerm absTerm 1734 def 1482 ref appTerm 1735 def appTerm refl 1734 ref 1637 ref 1483 ref appTerm 1736 def appTerm betaConv appThm 428 ref 1735 remove betaConv appThm 1679 ref 1736 ref appTerm refl appThm trans 1734 remove refl 1723 remove 1724 remove 902 ref subst subst 1737 def appThm eqMp appThm nil 1624 ref 1417 ref nil cons 1738 def cons 646 remove 914 remove cons nil cons cons nil cons cons 1739 def 338 remove "B" 1418 ref cons nil cons 1740 def cons 42 ref cons 1741 def 1025 ref subst subst eqMp eqMp eqMp 1742 def appThm eqMp 1626 ref 1417 ref appTerm refl 1743 def 1626 ref "_31888" 1458 remove var 1744 def 1629 ref 1637 ref 1645 ref 1744 remove varTerm appTerm appTerm appTerm absTerm 1745 def 1484 remove appTerm 1746 def appTerm refl 1745 ref 1667 remove appTerm betaConv appThm 1626 ref refl 1747 def 1746 remove betaConv appThm 1670 ref refl appThm trans 1745 remove refl 1711 remove appThm eqMp appThm 1743 ref 1626 ref "_31880" 1456 remove var 1748 def 1629 ref 1637 ref 1748 remove varTerm appTerm appTerm absTerm 1749 def 1483 remove appTerm 1750 def appTerm refl 1749 ref 1721 remove appTerm betaConv appThm 1747 ref 1750 remove betaConv appThm 1629 ref 1732 remove appTerm refl appThm trans 1749 remove refl 1722 remove appThm eqMp appThm 1743 remove 1626 ref "_31874" 1454 remove var 1751 def 1629 ref 1751 remove varTerm appTerm absTerm 1752 def 1482 remove appTerm 1753 def appTerm refl 1752 ref 1736 ref appTerm betaConv appThm 1747 remove 1753 remove betaConv appThm 1629 ref 1736 remove appTerm refl appThm trans 1752 remove refl 1737 remove appThm eqMp appThm 1739 remove 1741 remove 902 ref subst subst eqMp eqMp eqMp 1754 def appThm eqMp sym trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp 1541 ref 1542 remove 1594 ref nil cons 1755 def cons 1543 remove 1649 remove nil cons cons nil cons cons nil cons cons 382 ref subst proveHyp nil 103 ref 48 ref 1540 remove constTerm 1594 remove appTerm nil cons cons 104 ref 1610 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp nil "p" 1468 remove var 1755 remove cons nil cons nil cons cons 1541 remove 42 ref cons 900 ref subst subst eqMp eqMp nil 103 ref 21 ref 1608 ref appTerm nil cons cons 104 ref 1609 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 194 ref 195 ref 1608 remove nil cons cons 1131 ref cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 1607 remove nil cons cons 104 ref 1606 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 339 ref 337 ref 1605 remove nil cons cons 924 ref cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 1604 remove nil cons cons 104 ref 1603 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 339 ref 337 ref 1602 remove nil cons cons 926 ref cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 1601 remove nil cons cons 104 ref 1600 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 339 ref 337 ref 1599 remove nil cons cons 927 ref cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 1598 remove nil cons cons 104 ref 1597 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 1584 ref 1408 ref 1596 remove nil cons cons "x" 1406 ref var 1756 def 1738 remove cons nil cons 1757 def cons nil cons cons 185 ref subst eqMp eqMp 1489 ref refl 1490 ref 1587 ref 1425 ref 1587 ref 1426 ref 1491 ref refl 1492 remove betaConv appThm absThm appThm absThm appThm absThm appThm 1589 ref appThm trans appThm 1557 ref refl 1758 def 1409 ref 1502 ref 1500 remove "_31944" 1497 remove var 1759 def 21 ref 68 ref 214 ref 245 ref 214 ref 215 ref 214 ref 246 ref 1415 ref 1409 ref 1502 ref 1759 remove varTerm 1485 ref appTerm appTerm 1519 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 1760 def appTerm 1761 def 1485 ref appTerm appTerm 1519 ref appTerm absTerm 1762 def 1417 ref appTerm 1763 def betaConv 246 ref 1415 ref 1762 ref appTerm 1764 def absTerm 1765 def 249 ref appTerm 1766 def betaConv 215 ref 214 ref 1765 ref appTerm 1767 def absTerm 1768 def 219 ref appTerm 1769 def betaConv 245 ref 214 ref 1768 ref appTerm 1770 def absTerm 1771 def 248 ref appTerm 1772 def betaConv 68 ref 214 ref 1771 ref appTerm 1773 def absTerm 1774 def 1116 ref appTerm 1775 def betaConv 1760 ref 1761 remove appTerm 1776 def betaConv 1760 ref "_31942" 1460 ref var 1777 def 1506 ref 1507 ref 1415 ref 1425 ref 1415 ref 1426 ref 1508 ref 1435 ref 251 ref 1509 ref 1479 ref 1440 ref 255 ref 1699 ref 1648 ref 1777 remove varTerm appTerm 1778 def appTerm 1779 def appTerm appTerm 1779 remove appTerm appTerm 1511 ref 1481 ref 1690 remove 1645 remove 1778 remove appTerm 1780 def appTerm 1781 def appTerm 1432 ref appTerm appTerm appTerm appTerm absTerm 218 ref 1781 remove appTerm 1679 remove 1637 remove 1780 remove appTerm 1782 def appTerm appTerm appTerm absTerm 1443 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1444 ref 1629 remove 1782 remove appTerm appTerm appTerm absTerm 1783 def appTerm betaConv sym nil 195 ref 68 ref 214 ref 245 ref 214 ref 215 ref 214 ref 246 ref 1415 ref 1409 ref 1502 ref 1783 ref 1485 ref appTerm 1784 def appTerm 1519 remove appTerm 1785 def absTerm 1786 def appTerm 1787 def absTerm 1788 def appTerm 1789 def absTerm 1790 def appTerm 1791 def absTerm 1792 def appTerm 1793 def absTerm nil cons cons nil cons nil cons cons 344 ref subst 68 ref nil 8 ref 1793 remove nil cons cons nil cons nil cons cons 137 ref subst nil 337 ref 1792 remove nil cons cons nil cons nil cons cons 341 ref subst 245 ref nil 8 ref 1791 remove nil cons cons nil cons nil cons cons 137 ref subst nil 337 ref 1790 remove nil cons cons nil cons nil cons cons 341 ref subst 215 ref nil 8 ref 1789 remove nil cons cons nil cons nil cons cons 137 ref subst nil 337 ref 1788 remove nil cons cons nil cons nil cons cons 341 ref subst 246 ref nil 8 ref 1787 remove nil cons cons nil cons nil cons cons 137 ref subst nil 1408 ref 1786 remove nil cons cons nil cons nil cons cons 1585 ref subst 1409 ref nil 8 ref 1785 remove nil cons cons nil cons nil cons cons 137 ref subst 1784 remove betaConv 1502 ref "_31936" 1406 ref var 1794 def 1518 remove 1444 ref 1794 ref varTerm appTerm 1795 def appTerm absTerm 1417 ref appTerm 1796 def appTerm refl 1794 ref 1506 ref 1507 ref 1415 ref 1425 ref 1415 ref 1426 ref 1508 ref 1435 ref 251 ref 1509 ref 1479 ref 1440 ref 255 ref 1700 ref appTerm appTerm 1700 ref appTerm appTerm 1797 def 1511 ref 1481 ref 1691 ref appTerm 1432 ref appTerm appTerm appTerm appTerm absTerm 1798 def 218 ref 1691 ref appTerm 1799 def 1680 ref appTerm appTerm absTerm 1443 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1800 def 1795 ref appTerm absTerm 1801 def 1670 remove appTerm betaConv appThm 1502 ref refl 1802 def 1796 remove betaConv appThm 1800 remove 1671 remove appTerm refl appThm trans 13 ref 0 ref 0 ref 1406 ref 1477 remove cons opType 1803 def 0 ref 1803 ref 2 ref cons opType nil cons cons opType constTerm 1804 def "_31935" 201 ref var 1805 def 1794 ref 1506 ref 1507 ref 1415 ref 1425 ref 1415 ref 1426 ref 1508 ref 1435 ref 1516 remove 258 remove 1805 ref varTerm 1806 def appTerm appTerm absTerm 1443 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1795 ref appTerm absTerm absTerm 249 ref appTerm 1807 def appTerm refl 1805 ref 1794 ref 1506 ref 1507 ref 1415 ref 1425 ref 1415 ref 1426 ref 1508 ref 1435 ref 1798 remove 1799 remove 1806 ref appTerm appTerm absTerm 1443 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1795 ref appTerm absTerm absTerm 1808 def 1680 remove appTerm betaConv appThm 1804 ref refl 1809 def 1807 remove betaConv appThm 1801 remove refl appThm trans 13 ref 0 ref 0 ref 201 ref 1803 remove nil cons cons opType 1810 def 0 ref 1810 ref 2 ref cons opType nil cons cons opType constTerm 1811 def "_31934" 201 ref var 1812 def 1805 ref 1794 ref 1506 ref 1507 ref 1415 ref 1425 ref 1415 ref 1426 ref 1508 ref 1435 ref 251 ref 1509 ref 1510 remove 1511 remove 1481 remove 1812 ref varTerm 1813 def appTerm 1432 ref appTerm appTerm 1814 def appTerm appTerm absTerm 218 ref 1813 remove appTerm 1806 remove appTerm 1815 def appTerm absTerm 1443 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1795 ref appTerm absTerm absTerm absTerm 248 ref appTerm 1816 def appTerm refl 1812 ref 1805 ref 1794 ref 1506 ref 1507 ref 1415 ref 1425 ref 1415 ref 1426 ref 1508 ref 1435 ref 251 ref 1509 ref 1797 remove 1814 ref appTerm appTerm absTerm 1815 ref appTerm absTerm 1443 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1795 ref appTerm absTerm absTerm absTerm 1817 def 1691 remove appTerm betaConv appThm 1811 remove refl 1816 remove betaConv appThm 1808 remove refl appThm trans 13 ref 0 ref 0 ref 201 ref 1810 remove nil cons cons opType 1818 def 0 ref 1818 remove 2 ref cons opType nil cons cons opType constTerm 1819 def "_31933" 201 ref var 1820 def 1812 remove 1805 remove 1794 remove 1506 ref 1507 ref 1415 ref 1425 ref 1415 ref 1426 ref 1508 ref 1435 ref 251 ref 1509 remove 1479 ref 1440 remove 255 remove 1820 remove varTerm 1821 def appTerm appTerm 1821 remove appTerm appTerm 1814 remove appTerm appTerm absTerm 1815 remove appTerm absTerm 1443 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1795 remove appTerm absTerm absTerm absTerm absTerm 1822 def 219 ref appTerm 1823 def appTerm refl 1822 ref 1700 remove appTerm betaConv appThm 1819 remove refl 1823 remove betaConv appThm 1817 remove refl appThm trans 1822 remove refl 1714 ref appThm eqMp 1725 remove appThm eqMp 1742 remove appThm eqMp 1754 remove appThm eqMp sym trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp 1544 ref 1545 remove 1760 ref nil cons 1824 def cons 1546 remove 1783 remove nil cons cons nil cons cons nil cons cons 382 ref subst proveHyp nil 103 ref 48 ref 1535 remove constTerm 1760 remove appTerm nil cons cons 104 ref 1776 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp nil "p" 1498 remove var 1824 remove cons nil cons nil cons cons 1544 remove 42 ref cons 900 ref subst subst eqMp eqMp nil 103 ref 21 ref 1774 ref appTerm nil cons cons 104 ref 1775 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 194 ref 195 ref 1774 remove nil cons cons 1131 ref cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 1773 remove nil cons cons 104 ref 1772 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 339 ref 337 ref 1771 remove nil cons cons 924 ref cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 1770 remove nil cons cons 104 ref 1769 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 339 ref 337 ref 1768 remove nil cons cons 926 ref cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 1767 remove nil cons cons 104 ref 1766 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 339 ref 337 ref 1765 remove nil cons cons 927 ref cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 1764 remove nil cons cons 104 ref 1763 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 1584 ref 1408 ref 1762 remove nil cons cons 1757 ref cons nil cons cons 185 ref subst eqMp eqMp 1506 ref refl 1507 ref 1587 ref 1425 ref 1587 ref 1426 ref 1508 ref refl 1517 remove betaConv 251 ref 1478 ref 1443 ref appTerm 1825 def 1479 ref 253 ref 1443 ref appTerm 1826 def 256 remove appTerm 219 ref appTerm appTerm 1514 remove appTerm appTerm 1827 def absTerm 259 ref appTerm betaConv trans appThm absThm appThm absThm appThm absThm appThm 1589 ref appThm trans appThm appThm 1409 ref 209 ref 1526 remove "_31986" 1461 remove var 1828 def 21 ref 68 ref 214 ref 245 ref 214 ref 215 ref 214 ref 246 ref 1415 ref 1409 ref 209 ref 1828 remove varTerm 1485 ref appTerm appTerm 219 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 1829 def appTerm 1830 def 1485 ref appTerm appTerm 219 ref appTerm absTerm 1831 def 1417 ref appTerm 1832 def betaConv 246 ref 1415 ref 1831 ref appTerm 1833 def absTerm 1834 def 249 ref appTerm 1835 def betaConv 215 ref 214 ref 1834 ref appTerm 1836 def absTerm 1837 def 219 ref appTerm 1838 def betaConv 245 ref 214 ref 1837 ref appTerm 1839 def absTerm 1840 def 248 ref appTerm 1841 def betaConv 68 ref 214 ref 1840 ref appTerm 1842 def absTerm 1843 def 1116 ref appTerm 1844 def betaConv 1829 ref 1830 remove appTerm 1845 def betaConv 1829 ref "_31984" 1460 remove var 1846 def 1699 remove 1648 remove 1846 remove varTerm appTerm appTerm absTerm 1847 def appTerm betaConv sym nil 195 ref 68 ref 214 ref 245 ref 214 ref 215 ref 214 ref 246 ref 1415 ref 1409 ref 209 ref 1847 ref 1485 remove appTerm 1848 def appTerm 219 ref appTerm 1849 def absTerm 1850 def appTerm 1851 def absTerm 1852 def appTerm 1853 def absTerm 1854 def appTerm 1855 def absTerm 1856 def appTerm 1857 def absTerm nil cons cons nil cons nil cons cons 344 remove subst 68 ref nil 8 ref 1857 remove nil cons cons nil cons nil cons cons 137 ref subst nil 337 ref 1856 remove nil cons cons nil cons nil cons cons 341 ref subst 245 ref nil 8 ref 1855 remove nil cons cons nil cons nil cons cons 137 ref subst nil 337 ref 1854 remove nil cons cons nil cons nil cons cons 341 ref subst 215 ref nil 8 ref 1853 remove nil cons cons nil cons nil cons cons 137 ref subst nil 337 ref 1852 remove nil cons cons nil cons nil cons cons 341 remove subst 246 ref nil 8 ref 1851 remove nil cons cons nil cons nil cons cons 137 ref subst nil 1408 ref 1850 remove nil cons cons nil cons nil cons cons 1585 ref subst 1409 ref nil 8 ref 1849 remove nil cons cons nil cons nil cons cons 137 ref subst 1848 remove betaConv 1714 remove sym trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp 1547 ref 1548 ref 1829 ref nil cons 1858 def cons 1549 ref 1847 remove nil cons cons nil cons cons nil cons cons 382 ref subst proveHyp nil 103 ref 1465 remove 1829 remove appTerm nil cons cons 104 ref 1845 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp nil "p" 1463 remove var 1858 remove cons nil cons nil cons cons 1560 remove 900 ref subst subst eqMp eqMp nil 103 ref 21 ref 1843 ref appTerm nil cons cons 104 ref 1844 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 194 ref 195 remove 1843 remove nil cons cons 1131 remove cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 1842 remove nil cons cons 104 ref 1841 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 339 ref 337 ref 1840 remove nil cons cons 924 remove cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 1839 remove nil cons cons 104 ref 1838 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 339 ref 337 ref 1837 remove nil cons cons 926 ref cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 1836 remove nil cons cons 104 ref 1835 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 339 remove 337 remove 1834 remove nil cons cons 927 remove cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 1833 remove nil cons cons 104 ref 1832 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 1584 ref 1408 ref 1831 remove nil cons cons 1757 remove cons nil cons cons 185 ref subst eqMp eqMp appThm appThm 1586 remove 1424 ref 1587 ref 1425 ref 1587 remove 1426 ref 1588 remove 1591 remove betaConv 253 ref 6 ref 1443 ref appTerm 1116 ref appTerm 1859 def appTerm 219 ref appTerm 1860 def refl 251 ref 1557 ref 1827 remove appTerm absTerm 259 ref appTerm betaConv appThm trans appThm absThm appThm absThm appThm absThm appThm 1589 remove appThm appThm sym "x" 1419 ref var 1861 def 48 ref 1414 remove constTerm 1862 def "a" 1406 ref var 1863 def 1862 ref 1624 ref 13 ref 0 ref 1419 ref 1488 ref cons opType constTerm 1864 def 1861 ref varTerm appTerm 1429 remove 1863 ref varTerm 1865 def appTerm 1627 ref appTerm 1866 def appTerm absTerm appTerm absTerm appTerm absTerm 1867 def 1445 ref appTerm 1868 def betaConv 1583 remove 1740 remove cons 42 ref cons 1869 def nil 19 ref 0 ref 0 ref 695 ref 2 ref cons opType 1870 def 2 ref cons opType constTerm "x" 695 ref var 1871 def 49 remove 700 remove 1191 remove 84 remove 13 ref 0 ref 695 remove 1870 remove nil cons cons opType constTerm 1871 remove varTerm appTerm 702 remove appTerm absTerm appTerm absTerm appTerm absTerm appTerm axiom subst nil 103 ref 19 ref 1487 ref constTerm 1867 ref appTerm nil cons cons 104 ref 1868 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp "A" 1427 remove cons nil cons "P" 1486 ref var 1867 remove nil cons cons 1861 remove 1445 ref nil cons cons nil cons cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 1862 ref 1863 ref 1862 ref 1624 ref 1864 remove 1445 ref appTerm 1872 def 1866 ref appTerm absTerm appTerm absTerm 1873 def appTerm 1874 def nil cons cons 104 ref 209 ref 253 ref 1489 ref 1490 remove 1415 ref 1425 ref 1415 ref 1426 ref 1491 remove 35 ref 1859 ref appTerm 1875 def appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1876 def 1445 ref appTerm appTerm 1557 ref 1506 ref 1507 remove 1415 ref 1425 ref 1415 ref 1426 ref 1508 remove 1825 ref 1479 ref 1826 remove 218 remove 259 ref appTerm 219 ref appTerm 1877 def appTerm 219 ref appTerm appTerm 1878 def 1480 remove 259 ref appTerm 1879 def 1513 remove appTerm appTerm appTerm 1880 def appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1881 def 1445 ref appTerm appTerm appTerm 219 ref appTerm appTerm 1423 ref 1424 ref 1415 ref 1425 ref 1415 ref 1426 ref 1434 ref 1860 ref 1557 ref 1880 ref appTerm 1882 def appTerm 1883 def appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1884 def 1445 ref appTerm appTerm 1885 def nil cons 1886 def cons nil cons 1887 def cons nil cons cons 165 ref subst proveHyp nil 1408 ref 1425 ref 105 ref 1873 ref 1430 ref appTerm 1888 def appTerm 1885 ref appTerm 1889 def absTerm nil cons cons nil cons nil cons cons 1585 ref subst 1425 ref nil 8 ref 1889 remove nil cons cons nil cons nil cons cons 137 ref subst nil 103 ref 1888 ref nil cons 1890 def cons 1887 ref cons nil cons cons 1891 def 121 ref subst 1891 remove 178 ref subst 1888 ref betaConv 1888 remove assume eqMp nil 103 ref 1862 remove 1624 ref 1872 ref 1431 remove 1627 ref appTerm appTerm absTerm 1892 def appTerm 1893 def nil cons cons 1887 ref cons nil cons cons 165 ref subst proveHyp nil 1408 ref 1426 ref 105 ref 1892 ref 1432 ref appTerm 1894 def appTerm 1885 ref appTerm 1895 def absTerm nil cons cons nil cons nil cons cons 1585 ref subst 1426 ref nil 8 ref 1895 remove nil cons cons nil cons nil cons cons 137 ref subst nil 103 ref 1894 ref nil cons 1896 def cons 1887 ref cons nil cons cons 1897 def 121 ref subst 1897 remove 178 ref subst 1894 ref betaConv 1894 remove assume eqMp nil 103 ref 1872 remove 1433 ref appTerm 1898 def nil cons 1899 def cons 1887 remove cons nil cons cons 1900 def 165 ref subst proveHyp 1900 ref 121 ref subst 1900 remove 178 ref subst 14 ref "_31988" 1419 ref var 1901 def 209 ref 253 ref 1876 ref 1901 remove varTerm 1902 def appTerm appTerm 1557 ref 1881 ref 1902 ref appTerm appTerm appTerm 219 ref appTerm appTerm 1884 ref 1902 remove appTerm appTerm absTerm 1903 def 1445 ref appTerm 1904 def appTerm refl 1903 ref 1433 ref appTerm betaConv appThm 145 ref 1904 remove betaConv appThm 209 ref 253 ref 1876 remove 1433 ref appTerm appTerm 1557 ref 1881 remove 1433 ref appTerm appTerm appTerm 219 ref appTerm appTerm 1884 remove 1433 ref appTerm appTerm refl appThm trans 1903 remove refl 1898 remove assume appThm eqMp sym 428 ref 1592 ref 1426 ref 14 ref 1489 remove "_32000" 1486 ref var 1905 def 1415 ref 1425 ref 1415 ref 1426 ref 14 ref 1905 remove varTerm 1433 ref appTerm appTerm 1875 ref appTerm absTerm appTerm absTerm appTerm absTerm 1906 def appTerm 1907 def 1433 ref appTerm appTerm 1875 ref appTerm absTerm 1908 def 1432 ref appTerm 1909 def betaConv 1425 ref 1415 ref 1908 ref appTerm 1910 def absTerm 1911 def 1430 ref appTerm 1912 def betaConv 1906 ref 1907 remove appTerm 1913 def betaConv 1906 ref "_31998" 1419 ref var 1914 def 35 ref 6 ref 1442 ref 39 ref 0 ref 0 ref 0 ref 1419 ref 1418 remove cons opType 1915 def 2 ref cons opType 1915 ref nil cons cons opType constTerm 1916 def "fn" 1915 remove var 1917 def 1415 ref 1863 ref 1415 ref 1624 ref 1626 remove 1917 ref varTerm 1866 remove appTerm appTerm 1918 def 1865 remove appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1919 def 1914 remove varTerm appTerm appTerm appTerm 1116 ref appTerm appTerm absTerm 1920 def appTerm betaConv sym nil 1408 ref 1425 ref 1415 ref 1426 ref 14 ref 1920 ref 1433 ref appTerm 1921 def appTerm 1875 ref appTerm 1922 def absTerm 1923 def appTerm 1924 def absTerm nil cons cons nil cons nil cons cons 1585 ref subst 1425 ref nil 8 ref 1924 remove nil cons cons nil cons nil cons cons 137 ref subst nil 1408 ref 1923 remove nil cons cons nil cons nil cons cons 1585 ref subst 1426 ref nil 8 ref 1922 remove nil cons cons nil cons nil cons cons 137 ref subst 1921 remove betaConv 14 ref "_31995" 1406 ref var 1925 def 1875 ref absTerm 1432 ref appTerm 1926 def appTerm refl 1925 ref 35 ref 6 ref 1442 ref 1919 ref 1433 ref appTerm 1927 def appTerm 1928 def appTerm 1116 ref appTerm 1929 def appTerm 1930 def absTerm 1931 def 1916 remove 1917 remove 1415 ref 1863 ref 1415 ref 1624 ref 1918 remove 1627 remove appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1932 def 1433 ref appTerm 1933 def appTerm betaConv appThm 145 ref 1926 remove betaConv appThm 1930 remove refl appThm trans 1672 remove "_31994" 1406 ref var 1934 def 1925 remove 35 ref 6 ref 1442 ref 1934 remove varTerm appTerm appTerm 1116 ref appTerm appTerm absTerm absTerm 1935 def 1430 ref appTerm 1936 def appTerm refl 1935 ref 1927 ref appTerm betaConv appThm 1681 remove 1936 remove betaConv appThm 1931 remove refl appThm trans 1935 remove refl nil 1624 remove 1432 ref nil cons 1937 def cons 1863 remove 1430 ref nil cons 1938 def cons nil cons cons nil cons cons 1939 def 1869 ref 1025 remove subst subst 1940 def appThm eqMp 1939 remove 1869 remove 902 remove subst subst 1941 def appThm eqMp sym trans eqMp absThm eqMp eqMp absThm eqMp eqMp "A" 1488 remove cons nil cons 1942 def "P" 1487 ref var 1906 ref nil cons 1943 def cons "x" 1486 remove var 1920 remove nil cons cons nil cons cons nil cons cons 382 ref subst proveHyp nil 103 ref 48 ref 0 ref 1487 ref 2 ref cons opType constTerm 1906 remove appTerm nil cons cons 104 ref 1913 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp nil "p" 1487 remove var 1943 remove cons nil cons nil cons cons 1942 remove 42 ref cons 900 ref subst subst eqMp eqMp nil 103 ref 1415 ref 1911 ref appTerm nil cons cons 104 ref 1912 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 1584 ref 1408 ref 1911 remove nil cons cons 1756 ref 1938 remove cons nil cons 1944 def cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 1910 remove nil cons cons 104 ref 1909 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 1584 ref 1408 ref 1908 remove nil cons cons 1756 ref 1937 remove cons nil cons 1945 def cons nil cons cons 185 ref subst eqMp eqMp appThm 1758 remove 1426 ref 1502 ref 1506 remove "_32012" 1503 ref var 1946 def 1415 ref 1425 ref 1415 ref 1426 ref 1502 ref 1946 remove varTerm 1433 ref appTerm appTerm 1880 ref appTerm absTerm appTerm absTerm appTerm absTerm 1947 def appTerm 1948 def 1433 ref appTerm appTerm 1880 ref appTerm absTerm 1949 def 1432 ref appTerm 1950 def betaConv 1425 ref 1415 ref 1949 ref appTerm 1951 def absTerm 1952 def 1430 ref appTerm 1953 def betaConv 1947 ref 1948 remove appTerm 1954 def betaConv 1947 ref "_32010" 1419 ref var 1955 def 1478 ref 1442 ref 1919 ref 1955 remove varTerm 1956 def appTerm appTerm 1957 def appTerm 1479 ref 253 ref 1957 remove appTerm 1877 ref appTerm 219 ref appTerm appTerm 1879 ref 1512 ref 1932 ref 1956 remove appTerm appTerm appTerm appTerm appTerm absTerm 1958 def appTerm betaConv sym nil 1408 ref 1425 ref 1415 ref 1426 ref 1502 ref 1958 ref 1433 ref appTerm 1959 def appTerm 1880 remove appTerm 1960 def absTerm 1961 def appTerm 1962 def absTerm nil cons cons nil cons nil cons cons 1585 ref subst 1425 ref nil 8 ref 1962 remove nil cons cons nil cons nil cons cons 137 ref subst nil 1408 ref 1961 remove nil cons cons nil cons nil cons cons 1585 ref subst 1426 ref nil 8 ref 1960 remove nil cons cons nil cons nil cons cons 137 ref subst 1959 remove betaConv 1502 remove "_32007" 1406 ref var 1963 def 1825 ref 1878 ref 1879 ref 1512 ref 1963 ref varTerm appTerm appTerm 1964 def appTerm appTerm absTerm 1432 ref appTerm 1965 def appTerm refl 1963 ref 1478 ref 1928 ref appTerm 1966 def 1479 ref 253 ref 1928 remove appTerm 1877 ref appTerm 219 ref appTerm appTerm 1967 def 1964 ref appTerm appTerm absTerm 1968 def 1933 ref appTerm betaConv appThm 1802 remove 1965 remove betaConv appThm 1966 ref 1967 ref 1879 ref 1512 ref 1933 ref appTerm appTerm appTerm appTerm 1969 def refl appThm trans 1804 remove "_32006" 1406 ref var 1970 def 1963 remove 1478 ref 1442 ref 1970 remove varTerm appTerm 1971 def appTerm 1479 ref 253 ref 1971 remove appTerm 1877 ref appTerm 219 ref appTerm appTerm 1964 remove appTerm appTerm absTerm absTerm 1972 def 1430 ref appTerm 1973 def appTerm refl 1972 ref 1927 ref appTerm betaConv appThm 1809 remove 1973 remove betaConv appThm 1968 remove refl appThm trans 1972 remove refl 1940 ref appThm eqMp 1941 ref appThm eqMp sym trans eqMp absThm eqMp eqMp absThm eqMp eqMp "A" 1505 remove cons nil cons 1974 def "P" 1504 ref var 1947 ref nil cons 1975 def cons "x" 1503 remove var 1958 remove nil cons cons nil cons cons nil cons cons 382 ref subst proveHyp nil 103 ref 48 ref 0 ref 1504 ref 2 ref cons opType constTerm 1947 remove appTerm nil cons cons 104 ref 1954 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp nil "p" 1504 remove var 1975 remove cons nil cons nil cons cons 1974 remove 42 ref cons 900 ref subst subst eqMp eqMp nil 103 ref 1415 ref 1952 ref appTerm nil cons cons 104 ref 1953 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 1584 ref 1408 ref 1952 remove nil cons cons 1944 ref cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 1951 remove nil cons cons 104 ref 1950 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 1584 ref 1408 ref 1949 remove nil cons cons 1945 ref cons nil cons cons 185 ref subst eqMp eqMp appThm appThm 616 ref appThm appThm 1426 ref 209 ref 1423 ref "_32024" 1420 ref var 1976 def 1415 ref 1425 ref 1415 ref 1426 ref 209 ref 1976 remove varTerm 1433 ref appTerm appTerm 1883 ref appTerm absTerm appTerm absTerm appTerm absTerm 1977 def appTerm 1978 def 1433 ref appTerm appTerm 1883 ref appTerm absTerm 1979 def 1432 ref appTerm 1980 def betaConv 1425 ref 1415 ref 1979 ref appTerm 1981 def absTerm 1982 def 1430 ref appTerm 1983 def betaConv 1977 ref 1978 remove appTerm 1984 def betaConv 1977 ref "_32022" 1419 ref var 1985 def 253 ref 6 ref 1442 ref 1919 remove 1985 remove varTerm 1986 def appTerm appTerm 1987 def appTerm 1116 ref appTerm appTerm 219 ref appTerm 1557 ref 1478 ref 1987 ref appTerm 1479 ref 253 ref 1987 remove appTerm 1877 ref appTerm 219 ref appTerm appTerm 1879 ref 1512 ref 1932 remove 1986 remove appTerm appTerm appTerm appTerm appTerm appTerm appTerm absTerm 1988 def appTerm betaConv sym nil 1408 ref 1425 ref 1415 ref 1426 ref 209 ref 1988 ref 1433 ref appTerm 1989 def appTerm 1883 ref appTerm 1990 def absTerm 1991 def appTerm 1992 def absTerm nil cons cons nil cons nil cons cons 1585 ref subst 1425 ref nil 8 ref 1992 remove nil cons cons nil cons nil cons cons 137 ref subst nil 1408 ref 1991 remove nil cons cons nil cons nil cons cons 1585 ref subst 1426 ref nil 8 ref 1990 remove nil cons cons nil cons nil cons cons 137 ref subst 1989 remove betaConv 209 ref "_32019" 1406 ref var 1993 def 1860 remove 1557 ref 1825 remove 1878 remove 1879 remove 1512 remove 1993 ref varTerm appTerm appTerm 1994 def appTerm appTerm appTerm appTerm absTerm 1432 ref appTerm 1995 def appTerm refl 1993 ref 253 ref 1929 remove appTerm 219 ref appTerm 1996 def 1557 ref 1966 remove 1967 remove 1994 ref appTerm appTerm appTerm appTerm absTerm 1997 def 1933 remove appTerm betaConv appThm 428 ref 1995 remove betaConv appThm 1996 remove 1557 ref 1969 remove appTerm appTerm refl appThm trans 13 ref 0 ref 1411 ref 0 ref 1411 ref 2 ref cons opType nil cons cons opType constTerm 1998 def "_32018" 1406 ref var 1999 def 1993 remove 253 ref 6 remove 1442 remove 1999 remove varTerm appTerm 2000 def appTerm 1116 ref appTerm appTerm 219 ref appTerm 1557 remove 1478 remove 2000 ref appTerm 1479 remove 253 ref 2000 remove appTerm 1877 remove appTerm 219 ref appTerm appTerm 1994 remove appTerm appTerm appTerm appTerm absTerm absTerm 2001 def 1430 ref appTerm 2002 def appTerm refl 2001 ref 1927 remove appTerm betaConv appThm 1998 remove refl 2002 remove betaConv appThm 1997 remove refl appThm trans 2001 remove refl 1940 remove appThm eqMp 1941 remove appThm eqMp sym trans eqMp absThm eqMp eqMp absThm eqMp eqMp "A" 1422 remove cons nil cons 2003 def "P" 1421 ref var 1977 ref nil cons 2004 def cons "x" 1420 remove var 1988 remove nil cons cons nil cons cons nil cons cons 382 ref subst proveHyp nil 103 ref 48 remove 0 ref 1421 ref 2 ref cons opType constTerm 1977 remove appTerm nil cons cons 104 ref 1984 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp nil "p" 1421 remove var 2004 remove cons nil cons nil cons cons 2003 remove 42 ref cons 900 remove subst subst eqMp eqMp nil 103 ref 1415 ref 1982 ref appTerm nil cons cons 104 ref 1983 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 1584 ref 1408 ref 1982 remove nil cons cons 1944 remove cons nil cons cons 185 ref subst eqMp eqMp nil 103 ref 1981 remove nil cons cons 104 ref 1980 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 1584 ref 1408 ref 1979 remove nil cons cons 1945 remove cons nil cons cons 185 ref subst eqMp eqMp appThm sym nil 103 ref 14 ref 1859 ref appTerm 2005 def 474 ref appTerm 2006 def nil cons 2007 def cons 104 ref 209 ref 253 ref 1875 remove appTerm 1882 ref appTerm 219 ref appTerm appTerm 1883 remove appTerm nil cons 2008 def cons nil cons 2009 def cons nil cons cons 2010 def 121 ref subst 2010 remove 178 ref subst 14 remove "_32028" 1 ref var 2011 def 209 ref 253 ref 35 ref 2011 remove varTerm 2012 def appTerm appTerm 1882 ref appTerm 219 ref appTerm appTerm 253 ref 2012 remove appTerm 219 ref appTerm 1882 ref appTerm appTerm absTerm 2013 def 1859 ref appTerm 2014 def appTerm refl 2015 def 2013 ref 474 ref appTerm betaConv appThm 145 remove 2014 remove betaConv appThm 2016 def 209 ref 253 ref 1079 remove appTerm 1882 ref appTerm 219 ref appTerm appTerm 253 ref 474 ref appTerm 219 ref appTerm 1882 ref appTerm appTerm refl appThm trans 2013 remove refl 2017 def 2006 remove assume appThm eqMp sym 428 ref 1592 ref 1083 remove appThm 1882 ref refl 2018 def appThm 616 ref appThm nil "t2" 201 ref var 2019 def 909 ref cons "t1" 201 ref var 2020 def 1882 ref nil cons 2021 def cons nil cons cons nil cons cons 2022 def 340 ref 1103 remove subst 2023 def subst trans appThm nil 2019 remove 2021 ref cons 2020 remove 909 remove cons nil cons cons nil cons cons 2024 def 340 ref 1112 remove subst 2025 def subst appThm nil 923 remove 2021 remove cons nil cons nil cons cons 340 remove 1143 remove subst 2026 def subst trans sym 136 ref eqMp eqMp eqMp nil 142 ref 2007 ref cons 143 ref 2008 ref cons nil cons 2027 def cons nil cons cons 157 ref subst deductAntisym eqMp nil 103 ref 2005 remove 18 ref appTerm 2028 def nil cons 2029 def cons 2009 remove cons nil cons cons 2030 def 121 remove subst 2030 remove 178 remove subst 2015 remove "_32026" 1 remove var 2031 def 209 ref 253 ref 35 remove 2031 remove varTerm 2032 def appTerm appTerm 1882 ref appTerm 219 ref appTerm appTerm 253 ref 2032 remove appTerm 219 ref appTerm 1882 ref appTerm appTerm absTerm 18 ref appTerm betaConv appThm 2016 remove 209 ref 253 ref 1138 remove appTerm 1882 ref appTerm 219 ref appTerm appTerm 253 remove 18 remove appTerm 219 ref appTerm 1882 remove appTerm appTerm refl appThm trans 2017 remove 2028 remove assume appThm eqMp sym 428 remove 1592 remove 1141 remove appThm 2018 remove appThm 616 remove appThm 2022 remove 2025 remove subst trans appThm 2024 remove 2023 remove subst appThm nil 926 remove nil cons cons 2026 remove subst trans sym 136 remove eqMp eqMp eqMp nil 142 ref 2029 remove cons 2033 def 2027 remove cons nil cons cons 157 ref subst deductAntisym eqMp 1147 remove 1859 ref appTerm 2034 def betaConv 1150 remove nil 1151 remove 104 ref 2034 remove nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 194 remove 1152 remove 196 remove 1859 remove nil cons cons nil cons cons nil cons cons 185 remove subst eqMp eqMp nil 2033 remove 143 ref 2007 remove cons 1153 remove 2008 remove cons nil cons cons cons nil cons cons 1168 remove subst proveHyp proveHyp proveHyp eqMp eqMp eqMp nil 142 ref 1899 remove cons 143 ref 1886 remove cons nil cons 2035 def cons nil cons cons 157 ref subst deductAntisym eqMp eqMp eqMp nil 142 ref 1896 remove cons 2035 ref cons nil cons cons 157 ref subst deductAntisym eqMp eqMp absThm eqMp nil 103 ref 1415 ref 1756 ref 105 ref 1892 ref 1756 ref varTerm 2036 def appTerm appTerm 1885 ref appTerm absTerm appTerm nil cons cons 104 ref 105 ref 1893 remove appTerm 1885 ref appTerm nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 1584 ref 1408 ref 1892 remove nil cons cons 2035 ref cons nil cons cons 409 ref subst eqMp eqMp eqMp nil 142 ref 1890 remove cons 2035 ref cons nil cons cons 157 ref subst deductAntisym eqMp eqMp absThm eqMp nil 103 ref 1415 ref 1756 remove 105 ref 1873 ref 2036 remove appTerm appTerm 1885 ref appTerm absTerm appTerm nil cons cons 104 ref 105 ref 1874 remove appTerm 1885 remove appTerm nil cons cons nil cons cons nil cons cons 165 ref subst proveHyp 1584 remove 1408 ref 1873 remove nil cons cons 2035 remove cons nil cons cons 409 ref subst eqMp eqMp eqMp eqMp eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp 1451 remove "P" 1448 remove var 1446 remove nil cons cons "x" 1412 ref var 1571 remove nil cons cons nil cons cons nil cons cons 382 remove subst proveHyp eqMp nil 142 ref 1564 remove cons 143 remove 1554 remove cons nil cons 2037 def cons nil cons cons 157 ref subst deductAntisym eqMp eqMp eqMp nil 142 remove 1561 remove cons 2037 ref cons nil cons cons 157 remove subst deductAntisym eqMp eqMp absThm eqMp nil 103 remove 1530 remove 1549 ref 105 ref 1551 ref 1549 remove varTerm appTerm appTerm 1553 ref appTerm absTerm appTerm nil cons cons 104 remove 105 remove 1552 remove appTerm 1553 remove appTerm nil cons cons nil cons cons nil cons cons 165 remove subst proveHyp 1547 remove 1548 remove 1551 remove nil cons cons 2037 remove cons nil cons cons 409 remove subst eqMp eqMp eqMp eqMp defineConstList 2038 def pop hdTl pop 1412 remove constTerm 2039 def 474 remove appTerm 211 ref appTerm 212 ref appTerm 211 remove appTerm 2040 def 1410 ref varTerm 2041 def appTerm appTerm 212 ref appTerm 2042 def absTerm 2043 def defineConst 2044 def pop 1411 remove constTerm 2045 def 1417 ref appTerm appTerm 469 remove 2040 remove 1417 ref appTerm appTerm 212 remove appTerm appTerm absTerm 2046 def nil cons cons nil cons nil cons cons 1585 ref subst 1410 remove nil 8 ref 209 ref 2045 ref 2041 ref appTerm appTerm 2042 remove appTerm nil cons cons nil cons nil cons cons 137 ref subst 2044 remove 2041 ref refl appThm 2043 remove 2041 remove appTerm betaConv trans eqMp absThm eqMp nil 1415 ref 2046 remove appTerm thm 240 remove 241 remove 239 ref subst proveHyp nil 237 remove thm 199 remove 200 remove 239 ref subst proveHyp nil 198 remove thm nil "P" 0 ref 0 ref 1406 ref 53 remove cons opType 2047 def 2 ref cons opType 2048 def var "f" 2047 ref var 2049 def 1415 ref 1409 ref 13 remove 0 ref 72 remove 88 remove nil cons cons opType constTerm 2050 def "Data.List.Fibonacci.random" "_32035" 2047 ref var 2051 def "_32036" 1406 ref var 2052 def 39 remove 0 ref 0 ref 0 ref 1419 remove 90 ref cons opType 2053 def 2 ref cons opType 2053 ref nil cons cons opType constTerm 2054 def "f" 2053 remove var 2055 def 1415 ref 1425 ref 1415 ref 1426 ref 2050 ref 2055 ref varTerm 1433 remove appTerm appTerm 2056 def "Data.List.random" const 0 ref 2047 ref 0 ref 201 remove 0 ref 1406 remove 90 remove cons opType nil cons 2057 def cons opType nil cons cons opType constTerm 2058 def 2051 ref varTerm 2059 def appTerm 2045 remove 1430 remove appTerm 2060 def appTerm 1432 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1444 remove 2052 ref varTerm 2061 def appTerm appTerm 2062 def absTerm 2063 def absTerm 2064 def defineConst 2065 def pop 0 ref 2047 ref 2057 remove cons opType constTerm 2066 def 2049 remove varTerm 2067 def appTerm 1417 ref appTerm appTerm 2054 remove 2055 remove 1415 ref 1425 ref 1415 ref 1426 ref 2056 remove 2058 remove 2067 remove appTerm 2060 remove appTerm 1432 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1445 ref appTerm appTerm absTerm appTerm absTerm 2068 def nil cons cons nil cons nil cons cons "A" 2047 remove nil cons cons nil cons 42 remove cons 327 remove subst subst 2051 remove nil 8 ref 1415 ref 2052 ref 2050 remove 2066 remove 2059 ref appTerm 2061 ref appTerm appTerm 2062 remove appTerm 2069 def absTerm 2070 def appTerm nil cons cons nil cons nil cons cons 137 ref subst nil 1408 remove 2070 remove nil cons cons nil cons nil cons cons 1585 remove subst 2052 remove nil 8 remove 2069 remove nil cons cons nil cons nil cons cons 137 remove subst 2065 remove 2059 ref refl appThm 2064 remove 2059 remove appTerm betaConv trans 2061 ref refl appThm 2063 remove 2061 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp nil 19 remove 0 remove 2048 remove 2 remove cons opType constTerm 2068 remove appTerm thm 1389 remove nil 214 ref 215 ref 214 ref 245 ref 214 ref 246 ref 444 ref 1396 ref 248 ref appTerm 249 ref appTerm appTerm 251 ref 1175 remove 1396 remove 254 ref appTerm 248 ref appTerm appTerm absTerm 259 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm thm 437 remove 443 remove 239 remove subst proveHyp nil 442 remove thm 1170 remove nil 24 remove 458 remove 214 ref 215 ref 214 ref 245 ref 214 ref 246 ref 444 remove 1171 ref 460 remove appTerm 219 ref appTerm 248 ref appTerm 249 ref appTerm appTerm 463 remove 466 remove 1171 ref 468 remove appTerm 471 remove appTerm 249 ref appTerm 473 ref appTerm appTerm 1171 remove 476 remove appTerm 219 ref appTerm 249 ref appTerm 473 remove appTerm appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm thm 2038 remove nil 21 remove 68 remove 214 ref 215 remove 214 ref 245 remove 214 remove 246 remove 1415 ref 1409 remove 209 remove 2039 ref 1116 remove appTerm 219 remove appTerm 248 ref appTerm 249 remove appTerm 1417 remove appTerm appTerm 1423 remove 1424 remove 1415 ref 1425 remove 1415 remove 1426 remove 1434 remove 1435 remove 1439 remove 251 remove 2039 remove 1436 remove appTerm 1441 remove appTerm 254 remove appTerm 248 remove appTerm 1432 remove appTerm absTerm 259 remove appTerm appTerm absTerm 1443 remove appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1445 remove appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm thm