path: "vendor/opentheory/data/theories/natural-divides-gcd-def/natural-divides-gcd-def.art"
6 version "Data.Bool.!" const 0 def "->" typeOp 1 def 1 ref "Number.Natural.natural" typeOp nil opType 2 def "bool" typeOp nil opType 3 def nil cons 4 def cons opType 5 def 4 ref cons opType 6 def constTerm 7 def refl 8 def "a" 2 ref var 9 def "=" const 10 def 1 ref 3 ref 1 ref 3 ref 4 ref cons opType 11 def nil cons cons opType 12 def constTerm 13 def refl 14 def 8 ref "b" 2 ref var 15 def "Data.Bool./\\" const 12 ref constTerm 16 def refl 17 def 15 ref "Number.Natural.divides" const 1 ref 2 ref 5 ref nil cons cons opType 18 def constTerm 19 def "Number.Natural.gcd" "f" 1 ref 2 ref 1 ref 2 ref 2 ref nil cons 20 def cons 21 def opType 22 def nil cons 23 def cons opType 24 def var 25 def nil cons cons nil cons 25 ref 7 ref 9 ref 7 ref 15 ref 16 ref 19 ref 25 ref varTerm 26 def 9 ref varTerm 27 def appTerm 28 def 15 ref varTerm 29 def appTerm 30 def appTerm 31 def 27 ref appTerm appTerm 16 ref 31 remove 29 ref appTerm appTerm 7 ref "c" 2 ref var 32 def "Data.Bool.==>" const 12 ref constTerm 33 def 16 ref 19 ref 32 ref varTerm 34 def appTerm 35 def 27 ref appTerm appTerm 35 ref 29 ref appTerm appTerm appTerm 36 def 35 ref 30 remove appTerm appTerm absTerm appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm 37 def refl 38 def 10 ref 1 ref 24 ref 1 ref 24 ref 4 ref cons opType 39 def nil cons cons opType constTerm 26 ref appTerm "select" const 40 def 1 ref 39 ref 24 ref nil cons 41 def cons opType constTerm 42 def 37 ref appTerm appTerm assume sym appThm 37 ref 26 remove appTerm betaConv trans "A" 41 ref cons nil cons nil nil cons 43 def cons nil 10 ref 1 ref 1 ref 1 ref "A" varType 44 def 4 ref cons opType 45 def 4 ref cons opType 46 def 1 ref 46 ref 4 ref cons opType 47 def nil cons cons opType constTerm 48 def "Data.Bool.?" const 49 def 46 ref constTerm 50 def appTerm 51 def "p" 45 ref var 52 def 52 ref varTerm 53 def 40 ref 1 ref 45 ref 44 ref nil cons 54 def cons opType constTerm 53 ref appTerm appTerm 55 def absTerm appTerm axiom 56 def subst 38 remove appThm "p" 39 ref var 57 def 57 remove varTerm 58 def 42 remove 58 remove appTerm appTerm absTerm 37 remove appTerm betaConv trans 8 ref 9 ref 14 ref 8 ref 15 ref 49 ref 6 remove constTerm 59 def refl "g" 2 ref var 60 def 15 ref 60 ref 16 ref 19 ref 60 ref varTerm 61 def appTerm 62 def 27 ref appTerm appTerm 16 ref 62 remove 29 ref appTerm appTerm 7 ref 32 ref 36 ref 35 ref 61 ref appTerm appTerm absTerm appTerm appTerm appTerm absTerm 63 def absTerm 64 def 29 ref appTerm betaConv 65 def 61 ref refl appThm 63 ref 61 ref appTerm betaConv trans absThm appThm absThm appThm appThm 49 ref 1 ref 1 ref 22 ref 4 ref cons opType 66 def 4 ref cons opType constTerm refl 67 def "f" 22 ref var 68 def 8 ref 15 ref 65 remove 68 ref varTerm 69 def 29 ref appTerm 70 def refl appThm 63 ref 70 ref appTerm betaConv trans absThm appThm absThm appThm appThm nil "r" 18 ref var 64 remove nil cons cons nil cons nil cons cons "B" 20 ref cons 71 def "A" 20 ref cons 72 def nil cons 73 def cons 43 ref cons "r" 1 ref 44 ref 1 ref "B" varType 74 def 4 ref cons opType 75 def nil cons 76 def cons opType 77 def var 78 def 13 ref 0 ref 46 ref constTerm 79 def "x" 44 ref var 80 def 49 ref 1 ref 75 ref 4 ref cons opType 81 def constTerm "y" 74 ref var 82 def 78 remove varTerm 83 def 80 ref varTerm 84 def appTerm 85 def 82 remove varTerm appTerm absTerm appTerm absTerm appTerm appTerm 49 ref 1 ref 1 ref 1 ref 44 ref 74 ref nil cons 86 def cons 87 def opType 88 def 4 ref cons opType 89 def 4 ref cons opType 90 def constTerm 91 def "f" 88 ref var 92 def 79 ref 80 ref 85 remove 92 ref varTerm 93 def 84 ref appTerm 94 def appTerm absTerm appTerm absTerm appTerm appTerm absTerm 95 def 83 ref appTerm 96 def betaConv nil 0 ref 1 ref 1 ref 77 ref 4 ref cons opType 97 def 4 ref cons opType constTerm 95 ref appTerm 98 def axiom nil "p" 3 ref var 99 def 98 remove nil cons cons "q" 3 ref var 100 def 96 remove nil cons cons nil cons cons nil cons cons 13 ref 33 ref 99 ref varTerm 101 def appTerm 102 def 100 ref varTerm 103 def appTerm 104 def appTerm 105 def refl 99 ref 100 ref 13 ref 16 ref 101 ref appTerm 106 def 103 ref appTerm 107 def appTerm 108 def 101 ref appTerm absTerm 109 def absTerm 110 def 101 ref appTerm betaConv 103 ref refl 111 def appThm 109 remove 103 ref appTerm betaConv trans appThm nil 10 ref 1 ref 12 ref 1 ref 12 ref 4 ref cons opType 112 def nil cons cons opType constTerm 113 def 33 ref appTerm 110 remove appTerm axiom 101 ref refl 114 def appThm 111 ref appThm eqMp 115 def sym 116 def 108 remove refl 100 ref 10 ref 1 ref 112 ref 1 ref 112 remove 4 ref cons opType nil cons cons opType constTerm 117 def "f" 12 remove var 118 def 118 ref varTerm 119 def 101 ref appTerm 103 ref appTerm absTerm 120 def appTerm 118 ref 119 ref "Data.Bool.T" const 3 ref constTerm 121 def appTerm 121 ref appTerm absTerm 122 def appTerm absTerm 123 def 103 ref appTerm betaConv appThm 10 ref 1 ref 11 ref 1 ref 11 ref 4 ref cons opType 124 def nil cons cons opType constTerm 125 def 106 ref appTerm refl 99 ref 123 remove absTerm 126 def 101 ref appTerm betaConv appThm nil 113 remove 16 ref appTerm 126 ref appTerm axiom 127 def 114 remove appThm eqMp 111 ref appThm eqMp 128 def sym 118 ref 119 ref refl nil "t" 3 ref var 129 def 101 ref nil cons 130 def cons nil cons nil cons cons 13 ref 129 ref varTerm 131 def appTerm 121 ref appTerm assume sym nil 121 ref axiom 132 def eqMp 131 ref assume 132 ref deductAntisym deductAntisym 133 def subst 101 ref assume 134 def eqMp appThm nil 129 ref 103 ref nil cons 135 def cons nil cons nil cons cons 133 ref subst 103 ref assume 136 def eqMp appThm absThm eqMp 137 def nil "P" 3 ref var 138 def 130 ref cons 139 def "Q" 3 ref var 140 def 135 ref cons nil cons 141 def cons nil cons cons 14 ref 118 ref 119 remove 138 ref varTerm 142 def appTerm 143 def 140 ref varTerm 144 def appTerm absTerm 145 def 99 ref 100 ref 101 ref absTerm absTerm 146 def appTerm betaConv 146 ref 142 ref appTerm betaConv 144 ref refl 147 def appThm 100 ref 142 ref absTerm 144 ref appTerm betaConv trans trans appThm 122 ref 146 ref appTerm betaConv 146 ref 121 ref appTerm betaConv 121 ref refl 148 def appThm 100 ref 121 ref absTerm 121 ref appTerm betaConv trans trans appThm 13 ref 16 ref 142 ref appTerm 149 def 144 ref appTerm 150 def appTerm refl 100 ref 117 remove 118 remove 143 remove 103 ref appTerm absTerm appTerm 122 ref appTerm absTerm 144 ref appTerm betaConv appThm 125 ref 149 remove appTerm refl 126 remove 142 ref appTerm betaConv appThm 127 remove 142 ref refl 151 def appThm eqMp 147 ref appThm eqMp 150 remove assume eqMp 152 def 146 remove refl appThm eqMp sym 132 ref eqMp 153 def subst 154 def deductAntisym eqMp 115 remove 104 ref assume 155 def eqMp sym 134 ref eqMp 14 ref 120 remove 99 ref 100 ref 103 ref absTerm 156 def absTerm 157 def appTerm betaConv 157 ref 101 ref appTerm betaConv 111 remove appThm 156 ref 103 ref appTerm betaConv trans trans appThm 122 remove 157 ref appTerm betaConv 157 ref 121 ref appTerm betaConv 148 remove appThm 156 ref 121 ref appTerm betaConv trans trans 158 def appThm 128 remove 107 remove assume eqMp 157 ref refl 159 def appThm eqMp sym 132 ref eqMp 160 def proveHyp 161 def deductAntisym 162 def subst proveHyp "A" 77 ref nil cons cons nil cons "P" 97 remove var 95 remove nil cons cons "x" 77 remove var 83 remove nil cons cons nil cons cons nil cons cons nil 99 ref 79 ref "P" 45 ref var 163 def varTerm 164 def appTerm 165 def nil cons 166 def cons 100 ref 164 ref 84 ref appTerm 167 def nil cons 168 def cons nil cons cons nil cons cons 169 def 116 ref subst 169 remove 160 remove 137 remove deductAntisym 170 def subst 13 ref 167 ref appTerm refl 80 ref 121 ref absTerm 171 def 84 ref appTerm betaConv appThm 52 ref 10 ref 1 ref 45 ref 46 ref nil cons cons opType constTerm 53 ref appTerm 171 remove appTerm absTerm 172 def 164 ref appTerm betaConv 173 def nil 48 remove 79 ref appTerm 172 remove appTerm axiom 164 ref refl 174 def appThm 175 def 165 ref assume eqMp eqMp 84 ref refl 176 def appThm eqMp sym 132 ref eqMp eqMp nil 138 ref 166 remove cons 140 ref 168 ref cons nil cons cons nil cons cons 153 ref subst deductAntisym eqMp 177 def subst eqMp eqMp 178 def subst subst eqMp absThm appThm 14 ref 8 ref 9 ref 67 remove 68 ref 9 ref 68 remove 7 ref 15 ref 16 ref 19 remove 70 ref appTerm 179 def 27 ref appTerm appTerm 16 ref 179 remove 29 ref appTerm appTerm 7 ref 32 ref 36 ref 35 ref 70 remove appTerm appTerm absTerm appTerm appTerm appTerm absTerm appTerm absTerm 180 def absTerm 181 def 27 ref appTerm betaConv 182 def 69 ref refl appThm 180 ref 69 remove appTerm betaConv trans absThm appThm absThm appThm appThm 49 ref 1 ref 39 remove 4 ref cons opType constTerm refl 25 remove 8 ref 9 ref 182 remove 28 ref refl appThm 180 remove 28 remove appTerm betaConv trans absThm appThm absThm appThm appThm nil "r" 1 ref 2 ref 66 remove nil cons cons opType var 181 remove nil cons cons nil cons nil cons cons "B" 23 remove cons 73 ref cons 43 ref cons 178 remove subst subst eqMp trans nil 7 ref 9 ref 7 ref 15 ref 59 ref 63 remove appTerm absTerm appTerm absTerm appTerm axiom eqMp eqMp eqMp defineConstList 183 def pop hdTl pop 24 ref constTerm 27 ref appTerm 29 ref appTerm 184 def appTerm 185 def 27 ref appTerm absTerm 186 def 29 ref appTerm betaConv 187 def appThm 15 ref 16 ref 185 remove 29 ref appTerm 188 def appTerm 7 ref 32 ref 36 remove 35 remove 184 remove appTerm appTerm absTerm appTerm 189 def appTerm absTerm 190 def 29 ref appTerm betaConv 191 def appThm absThm appThm appThm 17 ref 8 ref 15 ref 187 remove absThm appThm appThm 8 ref 15 ref 191 remove absThm appThm appThm appThm nil "p" 5 ref var 192 def 186 ref nil cons cons "q" 5 ref var 193 def 190 remove nil cons cons nil cons cons nil cons cons 73 ref 43 ref cons 194 def "q" 45 ref var 195 def 13 ref 79 ref 80 ref 16 ref 53 ref 84 ref appTerm 196 def appTerm 195 remove varTerm 197 def 84 ref appTerm 198 def appTerm absTerm appTerm appTerm 16 ref 79 ref 80 ref 196 ref absTerm 199 def appTerm appTerm 79 ref 80 ref 198 remove absTerm appTerm appTerm appTerm absTerm 200 def 197 ref appTerm 201 def betaConv 52 ref 0 ref 47 remove constTerm 202 def 200 ref appTerm 203 def absTerm 204 def 53 ref appTerm 205 def betaConv nil 202 ref 204 ref appTerm 206 def axiom nil 99 ref 206 remove nil cons cons 100 ref 205 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp "A" 45 ref nil cons 207 def cons nil cons 208 def "P" 46 remove var 209 def 204 remove nil cons cons "x" 45 ref var 210 def 53 ref nil cons 211 def cons nil cons 212 def cons nil cons cons 177 ref subst eqMp eqMp nil 99 ref 203 remove nil cons cons 100 ref 201 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp 208 ref 209 ref 200 remove nil cons cons 210 remove 197 remove nil cons cons nil cons cons nil cons cons 177 ref subst eqMp eqMp subst 213 def subst eqMp 16 ref 7 ref 186 remove appTerm 214 def appTerm refl 14 ref 8 ref 15 ref 17 ref 15 ref 188 remove absTerm 215 def 29 ref appTerm betaConv 216 def appThm 15 ref 189 remove absTerm 217 def 29 ref appTerm betaConv 218 def appThm absThm appThm appThm 17 ref 8 ref 15 ref 216 remove absThm appThm appThm 8 ref 15 ref 218 remove absThm appThm appThm appThm nil 192 ref 215 ref nil cons cons 193 ref 217 ref nil cons cons nil cons cons nil cons cons 213 ref subst eqMp appThm trans absThm appThm 14 ref 8 ref 9 ref 17 ref 9 ref 214 remove absTerm 219 def 27 ref appTerm betaConv 220 def appThm 9 ref 16 ref 7 ref 215 remove appTerm 221 def appTerm 7 ref 217 remove appTerm 222 def appTerm absTerm 223 def 27 ref appTerm betaConv 224 def appThm absThm appThm appThm 17 ref 8 ref 9 ref 220 remove absThm appThm appThm 8 ref 9 ref 224 remove absThm appThm appThm appThm nil 192 ref 219 ref nil cons cons 193 ref 223 remove nil cons cons nil cons cons nil cons cons 213 ref subst eqMp 16 ref 7 ref 219 remove appTerm 225 def appTerm refl 14 ref 8 ref 9 ref 17 ref 9 ref 221 remove absTerm 226 def 27 ref appTerm betaConv 227 def appThm 9 ref 222 remove absTerm 228 def 27 ref appTerm betaConv 229 def appThm absThm appThm appThm 17 ref 8 ref 9 ref 227 remove absThm appThm appThm 8 ref 9 ref 229 remove absThm appThm appThm appThm nil 192 remove 226 ref nil cons cons 193 remove 228 ref nil cons cons nil cons cons nil cons cons 213 remove subst eqMp appThm trans trans 183 remove eqMp 230 def nil 138 ref 225 ref nil cons cons 140 ref 16 ref 7 ref 226 remove appTerm 231 def appTerm 7 ref 228 remove appTerm 232 def appTerm nil cons cons nil cons cons nil cons cons 233 def 153 ref subst proveHyp nil 225 remove thm 230 remove 233 remove 14 ref 145 remove 157 ref appTerm betaConv 157 remove 142 ref appTerm betaConv 147 remove appThm 156 remove 144 ref appTerm betaConv trans trans appThm 158 remove appThm 152 remove 159 remove appThm eqMp sym 132 ref eqMp 234 def subst proveHyp 235 def nil 138 ref 231 ref nil cons cons 140 ref 232 ref nil cons cons nil cons cons nil cons cons 236 def 153 ref subst proveHyp nil 231 remove thm 235 remove 236 remove 234 ref subst proveHyp nil 232 remove thm nil "P" 5 remove var 237 def 9 ref 7 ref 15 ref 7 ref "x" 2 ref var 238 def 7 ref "y" 2 ref var 239 def 10 ref 18 ref constTerm 240 def "Number.Natural.chineseRemainder" "_29368" 2 ref var 241 def "_29369" 2 ref var 242 def "_29370" 2 ref var 243 def "_29371" 2 ref var 244 def 40 ref 1 ref 1 ref 1 ref "Data.Pair.*" typeOp 245 def 2 ref 245 ref 21 remove opType 246 def nil cons 247 def cons 248 def opType 249 def 20 ref cons opType 250 def 4 ref cons opType 250 ref nil cons cons opType constTerm 251 def "f" 250 remove var 252 def 7 ref 60 ref 7 ref "s" 2 ref var 253 def 7 ref "t" 2 ref var 254 def 240 ref 252 ref varTerm "Data.Pair.," const 255 def 1 ref 2 ref 1 ref 246 ref 249 ref nil cons 256 def cons opType 257 def nil cons 258 def cons opType constTerm 259 def 61 remove appTerm 260 def 255 ref 1 ref 2 ref 1 ref 248 remove opType nil cons cons opType constTerm 261 def 253 ref varTerm 262 def appTerm 254 ref varTerm 263 def appTerm appTerm 264 def appTerm appTerm 265 def "Number.Natural.mod" const 24 ref constTerm 266 def "Number.Natural.+" const 24 ref constTerm 267 def "Number.Natural.*" const 24 ref constTerm 268 def 243 ref varTerm 269 def appTerm 268 ref "Number.Natural.-" const 24 ref constTerm 270 def 241 ref varTerm 271 def appTerm 263 ref appTerm appTerm 242 ref varTerm 272 def appTerm appTerm appTerm 268 ref 244 ref varTerm 273 def appTerm 268 ref 262 ref appTerm 274 def 271 ref appTerm appTerm appTerm appTerm 268 ref 271 ref appTerm 272 ref appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm "Number.Natural.egcd" "f" 1 ref 2 ref 1 ref 2 ref 256 ref cons opType 275 def nil cons cons opType 276 def var 277 def nil cons cons nil cons 277 ref 7 ref 9 ref 7 ref 15 ref 10 ref 1 ref 249 ref 1 ref 249 ref 4 ref cons opType 278 def nil cons cons opType constTerm 279 def 277 remove varTerm 280 def 27 ref appTerm 29 ref appTerm appTerm "Data.Bool.cond" const 281 def 1 ref 3 ref 1 ref 249 ref 1 ref 249 ref 256 ref cons opType 282 def nil cons 283 def cons opType nil cons cons opType constTerm 284 def 240 ref 29 ref appTerm "Number.Natural.zero" const 2 ref constTerm 285 def appTerm 286 def appTerm 259 ref 27 ref appTerm 261 ref "Number.Natural.bit1" const 22 remove constTerm 285 ref appTerm 287 def appTerm 288 def 285 ref appTerm 289 def appTerm 290 def appTerm 291 def 32 ref 284 ref 240 ref 34 ref appTerm 285 ref appTerm appTerm 292 def 259 ref 29 ref appTerm 288 ref 270 ref "Number.Natural.div" const 24 remove constTerm 293 def 27 ref appTerm 294 def 29 ref appTerm 295 def appTerm 287 ref appTerm appTerm appTerm 296 def appTerm 297 def 40 ref 1 ref 1 ref 282 ref 4 ref cons opType 283 remove cons opType constTerm 298 def "f" 282 remove var 299 def 7 ref 60 ref 7 ref 253 ref 7 ref 254 ref 279 ref 299 ref varTerm 264 remove appTerm appTerm 300 def "u" 2 ref var 301 def 260 ref 261 ref 301 ref varTerm 302 def appTerm 303 def 267 ref 263 ref appTerm 304 def 268 ref 295 remove appTerm 305 def 302 ref appTerm appTerm appTerm appTerm absTerm 306 def 267 ref 262 remove appTerm 307 def 268 ref 293 ref 29 ref appTerm 308 def 34 ref appTerm appTerm 263 ref appTerm appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 309 def 280 ref 34 ref appTerm 266 ref 29 ref appTerm 310 def 34 ref appTerm 311 def appTerm appTerm appTerm absTerm 266 ref 27 ref appTerm 312 def 29 ref appTerm 313 def appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm 314 def refl 315 def 10 ref 1 ref 276 ref 1 ref 276 ref 4 ref cons opType 316 def nil cons cons opType constTerm 280 ref appTerm 40 ref 1 ref 316 ref 276 ref nil cons 317 def cons opType constTerm 318 def 314 ref appTerm appTerm assume sym appThm 314 ref 280 remove appTerm betaConv trans "A" 317 remove cons nil cons 319 def 43 ref cons 56 remove subst 315 remove appThm "p" 316 ref var 320 def 320 remove varTerm 321 def 318 remove 321 remove appTerm appTerm absTerm 314 ref appTerm betaConv trans "B" 256 ref cons nil cons 43 ref cons "r" 1 ref 246 ref 1 ref 246 ref 4 ref cons opType 322 def nil cons cons opType 323 def var 324 def 33 ref "Relation.wellFounded" const 325 def 1 ref 323 ref 4 ref cons opType 326 def constTerm 327 def 324 remove varTerm 328 def appTerm appTerm 0 ref 1 ref 1 ref 1 ref 1 ref 246 ref 86 ref cons opType 329 def 329 ref nil cons cons opType 330 def 4 ref cons opType 4 ref cons opType constTerm "h" 330 remove var 331 def 33 ref 0 ref 1 ref 1 ref 329 ref 4 ref cons opType 4 ref cons opType 332 def constTerm 333 def "f" 329 ref var 334 def 333 remove "g" 329 remove var 335 def 0 ref 1 ref 322 ref 4 ref cons opType constTerm 336 def "x" 246 ref var 337 def 33 ref 336 ref "z" 246 ref var 338 def 33 ref 328 remove 338 ref varTerm 339 def appTerm 337 ref varTerm 340 def appTerm appTerm 10 ref 1 ref 74 ref 76 remove cons opType constTerm 341 def 334 ref varTerm 342 def 339 ref appTerm appTerm 335 remove varTerm 343 def 339 ref appTerm appTerm appTerm absTerm appTerm appTerm 341 ref 331 remove varTerm 344 def 342 ref appTerm 340 ref appTerm 345 def appTerm 344 remove 343 remove appTerm 340 ref appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm appTerm 49 ref 332 remove constTerm 334 remove 336 ref 337 ref 341 ref 342 remove 340 ref appTerm appTerm 345 remove appTerm absTerm appTerm absTerm appTerm appTerm absTerm appTerm appTerm absTerm 346 def "Relation.measure" const 347 def 1 ref 1 ref 246 ref 20 ref cons opType 348 def 323 ref nil cons 349 def cons opType constTerm "Data.Pair.snd" const 350 def 348 ref constTerm 351 def appTerm 352 def appTerm 353 def betaConv "A" 247 remove cons nil cons 354 def 43 ref cons 355 def nil 0 ref 1 ref 1 ref 1 ref 44 ref 207 remove cons opType 356 def 4 ref cons opType 357 def 4 ref cons opType constTerm "r" 356 ref var 358 def 33 ref 325 remove 357 remove constTerm 359 def 358 remove varTerm 360 def appTerm appTerm 0 ref 1 ref 1 ref 1 ref 88 ref 88 ref nil cons 361 def cons opType 362 def 4 ref cons opType 4 ref cons opType constTerm "h" 362 remove var 363 def 33 ref 0 ref 90 remove constTerm 364 def 92 ref 364 ref "g" 88 ref var 365 def 79 ref 80 ref 33 ref 79 ref "z" 44 ref var 366 def 33 ref 360 remove 366 remove varTerm 367 def appTerm 84 ref appTerm appTerm 341 ref 93 ref 367 ref appTerm appTerm 365 remove varTerm 368 def 367 remove appTerm appTerm appTerm absTerm appTerm appTerm 341 ref 363 remove varTerm 369 def 93 remove appTerm 84 ref appTerm 370 def appTerm 369 remove 368 remove appTerm 84 ref appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm appTerm 91 remove 92 remove 79 ref 80 ref 341 ref 94 remove appTerm 370 remove appTerm absTerm appTerm absTerm appTerm appTerm absTerm appTerm appTerm absTerm appTerm axiom subst nil 99 ref 0 ref 1 ref 326 ref 4 ref cons opType constTerm 346 ref appTerm nil cons cons 100 ref 353 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp "A" 349 remove cons nil cons "P" 326 remove var 346 remove nil cons cons "x" 323 remove var 352 ref nil cons cons nil cons cons nil cons cons 177 ref subst eqMp eqMp subst nil 99 ref 33 ref 327 remove 352 ref appTerm appTerm 0 ref 1 ref 1 ref 1 ref 257 ref 258 ref cons opType 371 def 4 ref cons opType 372 def 4 ref cons opType constTerm "h" 371 ref var 373 def 33 ref 0 ref 1 ref 1 ref 257 ref 4 ref cons opType 374 def 4 ref cons opType 375 def constTerm 376 def "f" 257 ref var 377 def 376 ref "g" 257 ref var 378 def 336 ref 337 ref 33 ref 336 ref 338 ref 33 ref 352 ref 339 ref appTerm 379 def 340 ref appTerm appTerm 380 def 279 ref 377 ref varTerm 381 def 339 ref appTerm appTerm 382 def 378 ref varTerm 383 def 339 ref appTerm appTerm appTerm absTerm appTerm appTerm 384 def 279 ref 373 remove varTerm 385 def 381 ref appTerm 340 ref appTerm 386 def appTerm 385 remove 383 ref appTerm 340 ref appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm appTerm 49 ref 375 remove constTerm 387 def 377 ref 336 ref 337 ref 279 ref 381 ref 340 ref appTerm appTerm 388 def 386 remove appTerm absTerm appTerm absTerm appTerm appTerm absTerm 389 def appTerm 390 def appTerm nil cons cons 100 ref 49 ref 1 ref 316 ref 4 ref cons opType constTerm 314 ref appTerm 391 def nil cons 392 def cons nil cons 393 def cons nil cons cons 162 ref subst proveHyp 33 ref refl 394 def 394 ref nil "m" 348 ref var 351 remove nil cons cons nil cons 395 def nil cons cons 355 ref nil 129 ref 359 remove 347 remove 1 ref 1 ref 44 ref 20 remove cons opType 396 def 356 ref nil cons cons opType constTerm "m" 396 ref var 397 def varTerm 398 def appTerm 399 def appTerm 400 def nil cons cons nil cons nil cons cons 133 ref subst 397 ref 400 remove absTerm 401 def 398 ref appTerm 402 def betaConv nil 0 ref 1 ref 1 ref 396 ref 4 ref cons opType 403 def 4 ref cons opType constTerm 404 def 401 ref appTerm 405 def axiom nil 99 ref 405 remove nil cons cons 100 ref 402 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp "A" 396 ref nil cons cons nil cons 406 def "P" 403 remove var 407 def 401 remove nil cons cons "x" 396 remove var 398 ref nil cons cons nil cons 408 def cons nil cons cons 177 ref subst eqMp eqMp eqMp subst subst appThm 390 ref refl appThm nil 129 ref 390 remove nil cons 409 def cons nil cons nil cons cons 129 ref 13 ref 33 ref 121 ref appTerm 131 ref appTerm appTerm 131 ref appTerm absTerm 410 def 131 ref appTerm 411 def betaConv nil 0 ref 124 remove constTerm 412 def 410 ref appTerm 413 def axiom nil 99 ref 413 remove nil cons cons 100 ref 411 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp "A" 4 ref cons nil cons 414 def "P" 11 ref var 415 def 410 remove nil cons cons "x" 3 ref var 416 def 131 ref nil cons cons nil cons 417 def cons nil cons cons 177 ref subst eqMp eqMp subst trans appThm 391 ref refl appThm sym nil 99 ref 409 ref cons 418 def 393 ref cons nil cons cons 419 def 116 ref subst 419 remove 170 ref subst 389 ref 377 ref 40 ref 1 ref 374 ref 258 ref cons opType constTerm 420 def "f'" 257 ref var 421 def 7 ref 9 ref 7 ref 15 ref 279 ref 421 remove varTerm 261 ref 27 ref appTerm 29 ref appTerm 422 def appTerm appTerm 291 ref 32 ref 297 ref 309 ref 381 ref 261 ref 34 ref appTerm 423 def 311 ref appTerm 424 def appTerm appTerm appTerm absTerm 313 ref appTerm 425 def appTerm 426 def appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 427 def appTerm 428 def betaConv nil 418 remove 100 ref 428 remove nil cons cons nil cons cons nil cons cons 162 ref subst "A" 371 ref nil cons cons nil cons "P" 372 remove var 389 remove nil cons cons "x" 371 remove var 427 ref nil cons cons nil cons cons nil cons cons 177 ref subst eqMp eqMp nil 99 ref 33 ref 376 ref 377 ref 376 ref 378 remove 336 ref 337 ref 384 remove 279 ref 427 ref 381 ref appTerm 429 def 340 ref appTerm 430 def appTerm 431 def 427 ref 383 remove appTerm 340 ref appTerm appTerm appTerm absTerm appTerm absTerm appTerm 432 def absTerm 433 def appTerm 434 def appTerm 387 ref 377 ref 336 ref 337 ref 388 remove 430 remove appTerm absTerm 435 def appTerm 436 def absTerm 437 def appTerm 438 def appTerm 439 def nil cons cons 393 ref cons nil cons cons 162 ref subst proveHyp nil "P" 374 ref var 440 def 433 remove nil cons cons nil cons nil cons cons "A" 258 remove cons nil cons 441 def 43 ref cons 442 def 13 ref 165 remove appTerm refl 173 remove appThm 175 remove eqMp sym 443 def subst 444 def subst 377 ref nil 129 ref 432 remove nil cons cons nil cons nil cons cons 133 ref subst nil 440 ref "h" 257 ref var 445 def 336 ref 337 ref 33 ref 336 ref 338 ref 380 remove 382 remove 445 ref varTerm 446 def 339 ref appTerm appTerm 447 def appTerm absTerm appTerm appTerm 431 remove 427 remove 446 ref appTerm 448 def 340 ref appTerm appTerm appTerm absTerm 449 def appTerm 450 def absTerm nil cons cons nil cons nil cons cons 444 ref subst 445 remove nil 129 ref 450 remove nil cons cons nil cons nil cons cons 133 ref subst 14 ref 336 remove refl 451 def 337 ref 449 ref 340 ref appTerm betaConv absThm appThm appThm 8 ref 9 ref 8 ref 15 ref 449 ref 422 ref appTerm betaConv absThm appThm absThm appThm appThm nil "p" 322 ref var 452 def 449 remove nil cons cons nil cons nil cons cons 72 remove 71 remove nil cons cons 43 ref cons 453 def "p" 1 ref 245 remove 87 remove opType 454 def 4 ref cons opType 455 def var 456 def 13 ref 0 ref 1 ref 455 ref 4 ref cons opType 457 def constTerm "x" 454 ref var 458 def 456 remove varTerm 459 def 458 remove varTerm appTerm absTerm appTerm appTerm 79 ref "a" 44 ref var 460 def 0 ref 81 remove constTerm 461 def "b" 74 ref var 462 def 459 ref 255 remove 1 ref 44 ref 1 ref 74 ref 454 ref nil cons cons opType nil cons cons opType constTerm 460 ref varTerm 463 def appTerm 462 ref varTerm 464 def appTerm 465 def appTerm absTerm appTerm absTerm appTerm appTerm absTerm 466 def 459 ref appTerm 467 def betaConv nil 0 ref 1 ref 457 ref 4 ref cons opType constTerm 466 ref appTerm 468 def axiom nil 99 ref 468 remove nil cons cons 100 ref 467 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp "A" 455 ref nil cons cons nil cons "P" 457 remove var 466 remove nil cons cons "x" 455 remove var 459 remove nil cons cons nil cons cons nil cons cons 177 ref subst eqMp eqMp subst 469 def subst eqMp 8 ref 9 ref 8 ref 15 ref 394 remove 14 ref 451 remove 338 ref 338 remove 33 ref 379 remove 422 ref appTerm appTerm 447 remove appTerm absTerm 470 def 339 remove appTerm betaConv absThm appThm appThm 8 ref "a'" 2 ref var 471 def 8 ref "b'" 2 ref var 472 def 470 ref 261 ref 471 ref varTerm appTerm 472 ref varTerm 473 def appTerm 474 def appTerm betaConv absThm appThm absThm appThm appThm nil 452 remove 470 remove nil cons cons nil cons nil cons cons 469 remove subst eqMp appThm 279 ref refl 475 def 429 remove betaConv 422 ref refl 476 def appThm 15 ref 279 ref 420 ref "_29340" 257 ref var 477 def 7 ref 9 ref 7 ref 15 ref 279 ref 477 remove varTerm 422 ref appTerm appTerm 426 ref appTerm absTerm appTerm absTerm appTerm absTerm 478 def appTerm 479 def 422 ref appTerm appTerm 426 ref appTerm absTerm 480 def 29 ref appTerm 481 def betaConv 9 ref 7 ref 480 ref appTerm 482 def absTerm 483 def 27 ref appTerm 484 def betaConv 478 ref 479 remove appTerm 485 def betaConv 478 ref "_29338" 246 ref var 486 def 284 ref 240 ref 40 ref 1 ref 1 ref 348 ref 4 ref cons opType 348 ref nil cons cons opType constTerm 487 def "fn" 348 remove var 488 def 7 ref 9 ref 7 ref 15 ref 240 ref 488 ref varTerm 422 ref appTerm appTerm 489 def 29 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm 490 def 486 remove varTerm 491 def appTerm 492 def appTerm 285 ref appTerm appTerm 259 ref 487 remove 488 remove 7 ref 9 ref 7 ref 15 ref 489 remove 27 ref appTerm absTerm appTerm absTerm appTerm absTerm appTerm 493 def 491 remove appTerm 494 def appTerm 289 ref appTerm appTerm 32 ref 292 ref 259 ref 492 ref appTerm 288 ref 270 ref 293 ref 494 ref appTerm 492 ref appTerm 495 def appTerm 287 ref appTerm appTerm appTerm appTerm 298 ref 299 ref 7 ref 60 ref 7 ref 253 ref 7 ref 254 ref 300 ref 301 ref 260 ref 303 ref 304 ref 268 ref 495 remove appTerm 302 ref appTerm appTerm appTerm appTerm absTerm 307 ref 268 ref 293 ref 492 ref appTerm 34 ref appTerm appTerm 263 ref appTerm appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 381 ref 423 ref 266 ref 492 ref appTerm 34 ref appTerm appTerm appTerm appTerm appTerm absTerm 266 ref 494 remove appTerm 492 remove appTerm appTerm appTerm absTerm 496 def appTerm betaConv sym nil 237 ref 9 ref 7 ref 15 ref 279 ref 496 ref 422 ref appTerm 497 def appTerm 426 ref appTerm 498 def absTerm 499 def appTerm 500 def absTerm nil cons cons nil cons nil cons cons 194 remove 443 ref subst 501 def subst 9 ref nil 129 ref 500 remove nil cons cons nil cons nil cons cons 133 ref subst nil 237 ref 499 remove nil cons cons nil cons nil cons cons 501 ref subst 15 ref nil 129 ref 498 remove nil cons cons nil cons nil cons cons 133 ref subst 497 remove betaConv 279 ref "_29335" 2 ref var 502 def 284 ref 240 ref 502 ref varTerm 503 def appTerm 285 ref appTerm appTerm 504 def 290 ref appTerm 32 ref 292 ref 259 ref 503 ref appTerm 505 def 288 ref 270 ref 294 ref 503 ref appTerm 506 def appTerm 287 ref appTerm appTerm appTerm appTerm 298 ref 299 ref 7 ref 60 ref 7 ref 253 ref 7 ref 254 ref 300 ref 301 ref 260 ref 303 ref 304 ref 268 ref 506 remove appTerm 302 ref appTerm appTerm appTerm appTerm absTerm 307 ref 268 ref 293 ref 503 ref appTerm 34 ref appTerm appTerm 263 ref appTerm appTerm 507 def appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 381 ref 423 ref 266 ref 503 ref appTerm 34 ref appTerm appTerm appTerm 508 def appTerm appTerm absTerm 312 ref 503 ref appTerm appTerm appTerm absTerm 29 ref appTerm 509 def appTerm refl 502 ref 504 ref 259 ref 493 ref 422 ref appTerm 510 def appTerm 289 ref appTerm 511 def appTerm 32 ref 292 ref 505 ref 288 ref 270 ref 293 ref 510 ref appTerm 512 def 503 ref appTerm 513 def appTerm 287 ref appTerm appTerm appTerm appTerm 298 ref 299 ref 7 ref 60 ref 7 ref 253 ref 7 ref 254 ref 300 ref 301 ref 260 ref 303 ref 304 ref 268 ref 513 remove appTerm 302 ref appTerm appTerm appTerm appTerm absTerm 507 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 508 ref appTerm appTerm absTerm 266 ref 510 ref appTerm 514 def 503 ref appTerm appTerm appTerm absTerm 515 def 490 ref 422 ref appTerm 516 def appTerm betaConv appThm 475 ref 509 remove betaConv appThm 284 ref 240 ref 516 ref appTerm 285 ref appTerm appTerm 511 ref appTerm 517 def 32 ref 292 ref 259 ref 516 ref appTerm 288 ref 270 ref 512 ref 516 ref appTerm 518 def appTerm 287 ref appTerm appTerm appTerm appTerm 519 def 298 ref 299 ref 7 ref 60 ref 7 ref 253 ref 7 ref 254 ref 300 ref 301 ref 260 ref 303 ref 304 ref 268 ref 518 remove appTerm 302 ref appTerm appTerm appTerm appTerm absTerm 307 ref 268 ref 293 ref 516 ref appTerm 34 ref appTerm appTerm 263 ref appTerm appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 520 def 381 ref 423 ref 266 ref 516 ref appTerm 34 ref appTerm appTerm 521 def appTerm appTerm appTerm absTerm 514 ref 516 ref appTerm 522 def appTerm appTerm refl appThm trans 10 ref 1 ref 275 ref 1 ref 275 remove 4 ref cons opType nil cons cons opType constTerm 523 def "_29334" 2 ref var 524 def 502 remove 504 remove 259 ref 524 remove varTerm 525 def appTerm 289 ref appTerm appTerm 32 ref 292 ref 505 remove 288 ref 270 ref 293 ref 525 ref appTerm 503 ref appTerm 526 def appTerm 287 ref appTerm appTerm appTerm appTerm 298 ref 299 ref 7 ref 60 ref 7 ref 253 ref 7 ref 254 ref 300 ref 301 ref 260 ref 303 ref 304 ref 268 ref 526 remove appTerm 302 ref appTerm appTerm appTerm appTerm absTerm 507 remove appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 508 remove appTerm appTerm absTerm 266 ref 525 remove appTerm 503 remove appTerm appTerm appTerm absTerm absTerm 527 def 27 ref appTerm 528 def appTerm refl 527 ref 510 ref appTerm betaConv appThm 523 ref refl 529 def 528 remove betaConv appThm 515 remove refl appThm trans 527 remove refl 453 ref 462 ref 10 ref 356 remove constTerm 530 def 40 ref 1 ref 1 ref 1 ref 454 ref 54 ref cons opType 531 def 4 ref cons opType 532 def 531 ref nil cons 533 def cons opType constTerm "fn" 531 remove var 534 def 79 ref 460 ref 461 ref 462 ref 530 ref 534 ref varTerm 465 ref appTerm appTerm 535 def 463 ref appTerm absTerm appTerm absTerm appTerm absTerm 536 def appTerm 537 def 465 ref appTerm appTerm 463 ref appTerm absTerm 538 def 464 ref appTerm 539 def betaConv 460 ref 461 ref 538 ref appTerm 540 def absTerm 541 def 463 ref appTerm 542 def betaConv 536 ref 537 remove appTerm 543 def betaConv 49 ref 1 ref 532 ref 4 ref cons opType constTerm 544 def refl 534 remove 79 ref refl 545 def 460 ref 461 ref refl 546 def 462 ref 535 remove refl 460 ref 462 ref 463 ref absTerm 547 def absTerm 548 def 463 ref appTerm betaConv 464 ref refl 549 def appThm 547 remove 464 ref appTerm betaConv trans appThm absThm appThm absThm appThm absThm appThm "C" 54 ref cons nil cons "_1343" 1 ref 44 ref 1 ref 74 ref 54 ref cons opType nil cons cons opType var 548 remove nil cons cons nil cons nil cons cons nil "f" 1 ref 44 ref 1 ref 74 ref "C" varType 550 def nil cons 551 def cons opType nil cons cons opType 552 def var 553 def 460 ref 462 ref "_1343" 552 ref var varTerm 463 ref appTerm 464 ref appTerm 554 def absTerm 555 def absTerm 556 def nil cons cons nil cons nil cons cons 553 ref 49 ref 1 ref 1 ref 1 ref 454 ref 551 remove cons opType 557 def 4 ref cons opType 558 def 4 ref cons opType 559 def constTerm 560 def "fn" 557 ref var 561 def 79 ref 460 ref 461 ref 462 ref 10 ref 1 ref 550 ref 1 ref 550 remove 4 ref cons opType nil cons cons opType constTerm 561 ref varTerm 562 def 465 ref appTerm appTerm 563 def 553 remove varTerm 564 def 463 ref appTerm 464 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 565 def 564 ref appTerm 566 def betaConv nil 0 ref 1 ref 1 ref 552 ref 4 ref cons opType 567 def 4 ref cons opType constTerm 565 ref appTerm 568 def axiom nil 99 ref 568 remove nil cons cons 100 ref 566 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp "A" 552 ref nil cons cons nil cons "P" 567 remove var 565 remove nil cons cons "x" 552 remove var 564 remove nil cons cons nil cons cons nil cons cons 177 ref subst eqMp eqMp subst nil 99 ref 560 ref 561 ref 79 ref 460 ref 461 ref 462 ref 563 ref 556 remove 463 ref appTerm 569 def 464 ref appTerm appTerm absTerm appTerm absTerm appTerm 570 def absTerm 571 def appTerm 572 def nil cons cons 100 ref 560 remove 561 ref 79 ref 460 ref 461 ref 462 ref 563 ref 554 remove appTerm absTerm appTerm absTerm appTerm absTerm 573 def appTerm 574 def nil cons 575 def cons nil cons 576 def cons nil cons cons 162 ref subst nil "P" 558 remove var 577 def 561 ref 33 ref 571 ref 562 ref appTerm 578 def appTerm 574 ref appTerm 579 def absTerm nil cons cons nil cons nil cons cons "A" 557 ref nil cons cons nil cons 580 def 43 ref cons 443 ref subst subst 561 remove nil 129 ref 579 remove nil cons cons nil cons nil cons cons 133 ref subst nil 99 ref 578 ref nil cons 581 def cons 576 ref cons nil cons cons 582 def 116 ref subst 582 remove 170 ref subst 578 ref betaConv 578 remove assume eqMp nil 99 ref 570 ref nil cons 583 def cons 576 remove cons nil cons cons 584 def 162 ref subst proveHyp 584 ref 116 ref subst 584 remove 170 ref subst 573 ref 562 ref appTerm betaConv sym 545 ref 460 ref 546 ref 462 ref 563 remove refl 569 remove betaConv 549 ref appThm 555 remove 464 ref appTerm betaConv trans appThm absThm appThm absThm appThm 570 remove assume eqMp eqMp 580 ref 577 ref 573 remove nil cons cons "x" 557 remove var 585 def 562 remove nil cons cons nil cons cons nil cons cons 13 ref 50 ref 164 ref appTerm 586 def appTerm 587 def refl 52 ref 412 ref 100 ref 33 ref 79 ref 80 ref 33 ref 196 ref appTerm 588 def 103 ref appTerm absTerm appTerm appTerm 103 ref appTerm absTerm appTerm absTerm 589 def 164 remove appTerm betaConv appThm nil 51 remove 589 remove appTerm axiom 174 remove appThm eqMp 590 def sym nil 415 ref 140 ref 33 ref 79 ref 80 ref 33 ref 167 ref appTerm 591 def 144 ref appTerm 592 def absTerm 593 def appTerm 594 def appTerm 595 def 144 ref appTerm 596 def absTerm nil cons cons nil cons nil cons cons 414 ref 43 ref cons 443 ref subst 597 def subst 140 ref nil 129 ref 596 remove nil cons cons nil cons nil cons cons 133 ref subst nil 99 ref 594 ref nil cons 598 def cons 599 def 100 ref 144 ref nil cons 600 def cons nil cons 601 def cons nil cons cons 602 def 116 ref subst 602 ref 170 ref subst nil 99 ref 168 ref cons 601 ref cons nil cons cons 603 def 162 ref subst 604 def 593 ref 84 ref appTerm 605 def betaConv nil 599 ref 100 ref 605 remove nil cons cons nil cons cons nil cons cons 162 ref subst "A" 54 ref cons 606 def nil cons 607 def 163 ref 593 remove nil cons cons 608 def 80 ref 84 ref nil cons cons nil cons 609 def cons nil cons cons 177 ref subst eqMp eqMp 610 def eqMp eqMp nil 138 ref 598 ref cons 611 def 140 ref 600 ref cons nil cons 612 def cons nil cons cons 153 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp 613 def subst proveHyp eqMp nil 138 ref 583 remove cons 140 ref 575 remove cons nil cons 614 def cons nil cons cons 153 ref subst deductAntisym eqMp eqMp eqMp nil 138 ref 581 remove cons 614 ref cons nil cons cons 153 ref subst deductAntisym eqMp eqMp absThm eqMp nil 99 ref 0 remove 559 remove constTerm 585 ref 33 ref 571 ref 585 remove varTerm appTerm appTerm 574 ref appTerm absTerm appTerm nil cons cons 100 ref 33 ref 572 remove appTerm 574 remove appTerm nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp 580 remove 577 remove 571 remove nil cons cons 614 remove cons nil cons cons nil 599 ref 100 ref 33 ref 586 ref appTerm 615 def 144 ref appTerm nil cons 616 def cons nil cons cons nil cons cons 617 def 116 ref subst 617 remove 170 ref subst nil 99 ref 586 remove nil cons 618 def cons 619 def 601 ref cons nil cons cons 620 def 116 ref subst 620 remove 170 ref subst 602 remove 162 ref subst 100 ref 33 ref 79 ref 80 ref 591 remove 103 ref appTerm absTerm appTerm appTerm 103 ref appTerm absTerm 621 def 144 ref appTerm 622 def betaConv nil 619 remove 100 ref 412 ref 621 ref appTerm 623 def nil cons 624 def cons nil cons cons nil cons cons 625 def 162 ref subst 590 remove nil 99 ref 587 remove 623 ref appTerm nil cons cons 100 ref 615 remove 623 remove appTerm nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp 625 remove nil 99 ref 13 ref 101 ref appTerm 626 def 103 ref appTerm 627 def nil cons 628 def cons 629 def 100 ref 104 ref nil cons 630 def cons nil cons 631 def cons nil cons cons 632 def 116 ref subst 632 remove 170 ref subst 116 ref 170 ref 627 remove assume 633 def 134 remove eqMp eqMp 154 ref deductAntisym eqMp 634 def eqMp nil 138 ref 628 remove cons 635 def 140 ref 630 ref cons nil cons 636 def cons nil cons cons 153 ref subst deductAntisym eqMp 637 def subst eqMp eqMp nil 99 ref 624 remove cons 100 ref 622 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp 414 ref 415 ref 621 remove nil cons cons 416 ref 600 remove cons nil cons cons nil cons cons 177 ref subst eqMp eqMp eqMp eqMp nil 138 ref 618 remove cons 612 ref cons nil cons cons 153 ref subst deductAntisym eqMp eqMp nil 611 ref 140 ref 616 remove cons nil cons cons nil cons cons 153 ref subst deductAntisym eqMp 638 def subst eqMp eqMp proveHyp 639 def subst eqMp nil 99 ref 544 remove 536 ref appTerm nil cons cons 100 ref 543 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp "A" 533 remove cons nil cons "p" 532 remove var 536 remove nil cons cons nil cons nil cons cons nil 99 ref 50 ref 53 ref appTerm 640 def nil cons 641 def cons 642 def 100 ref 13 ref 55 ref appTerm 643 def 121 ref appTerm 644 def nil cons 645 def cons nil cons 646 def cons nil cons cons 647 def 116 ref subst 647 remove 170 ref subst 50 ref refl nil "t" 45 ref var 211 ref cons nil cons nil cons cons 606 remove "B" 4 ref cons nil cons cons 43 ref cons "t" 88 ref var 648 def 10 remove 1 ref 88 ref 89 ref nil cons cons opType constTerm 80 ref 648 remove varTerm 649 def 84 ref appTerm absTerm appTerm 649 ref appTerm absTerm 650 def 649 ref appTerm 651 def betaConv nil 364 remove 650 ref appTerm 652 def axiom nil 99 ref 652 remove nil cons cons 100 ref 651 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp "A" 361 remove cons nil cons "P" 89 remove var 650 remove nil cons cons "x" 88 remove var 649 remove nil cons cons nil cons cons nil cons cons 177 ref subst eqMp eqMp subst subst appThm nil 129 ref 641 ref cons nil cons nil cons cons 653 def 133 ref subst 640 ref assume eqMp trans sym 132 ref eqMp nil 99 ref 50 ref 199 remove appTerm nil cons cons 646 ref cons nil cons cons 162 ref subst proveHyp nil 163 ref 211 remove cons 140 ref 645 remove cons nil cons 654 def cons nil cons cons nil 599 remove 100 ref 33 ref 50 remove 80 ref 167 ref absTerm 655 def appTerm 656 def appTerm 144 ref appTerm 657 def nil cons 658 def cons nil cons 659 def cons nil cons cons 660 def 634 remove nil 99 ref 630 ref cons 661 def 100 ref 33 ref 103 ref appTerm 662 def 101 ref appTerm nil cons 663 def cons nil cons 664 def cons nil cons cons 170 ref subst proveHyp 662 ref refl 633 remove appThm sym nil 99 ref 135 ref cons 665 def 100 ref 135 ref cons nil cons 666 def cons nil cons cons 667 def 116 ref subst 667 remove 170 ref subst 136 remove eqMp nil 138 ref 135 remove cons 141 ref cons nil cons cons 153 ref subst deductAntisym eqMp eqMp 668 def eqMp nil 665 ref 100 ref 130 ref cons nil cons 669 def cons nil cons cons 162 ref subst nil 138 ref 630 remove cons 670 def 140 ref 663 remove cons nil cons 671 def cons nil cons cons 672 def 234 ref subst eqMp 162 ref 672 remove 153 ref subst eqMp deductAntisym deductAntisym 673 def subst 660 ref 116 ref subst 660 remove 170 ref subst nil 163 ref 80 ref 33 ref 655 ref 84 ref appTerm 674 def appTerm 144 remove appTerm 675 def absTerm 676 def nil cons cons nil cons nil cons cons 443 ref subst 80 ref nil 129 ref 675 remove nil cons cons nil cons nil cons cons 133 ref subst nil 99 ref 674 ref nil cons 677 def cons 601 ref cons nil cons cons 678 def 116 ref subst 678 remove 170 ref subst 674 ref betaConv 679 def 674 remove assume eqMp 604 remove proveHyp 610 remove eqMp eqMp nil 138 ref 677 remove cons 612 ref cons nil cons cons 153 ref subst deductAntisym eqMp eqMp absThm eqMp nil 99 ref 79 ref 676 remove appTerm nil cons cons 659 remove cons nil cons cons 162 ref subst proveHyp 607 ref 163 ref 655 remove nil cons cons 680 def 612 ref cons nil cons cons 638 ref subst eqMp eqMp nil 611 remove 140 ref 658 ref cons nil cons cons nil cons cons 153 ref subst deductAntisym eqMp nil 99 ref 595 remove 657 ref appTerm nil cons cons 100 ref 33 ref 657 ref appTerm 594 remove appTerm nil cons cons nil cons cons nil cons cons 170 ref subst proveHyp nil 99 ref 658 ref cons 100 ref 598 ref cons nil cons cons nil cons cons 681 def 116 ref subst 681 remove 170 ref subst nil 608 remove nil cons nil cons cons 443 ref subst 80 ref nil 129 ref 592 remove nil cons cons nil cons nil cons cons 133 ref subst 603 ref 116 ref subst 603 remove 170 ref subst 679 remove sym 167 remove assume eqMp 607 ref 680 remove 609 ref cons nil cons cons 613 ref subst proveHyp nil 99 ref 656 remove nil cons cons 601 remove cons nil cons cons 162 ref subst 657 remove assume eqMp proveHyp eqMp nil 138 ref 168 remove cons 612 remove cons nil cons cons 153 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp nil 138 ref 658 remove cons 140 ref 598 remove cons nil cons cons nil cons cons 153 ref subst deductAntisym eqMp eqMp eqMp subst nil 163 ref 80 ref 588 ref 644 ref appTerm 682 def absTerm nil cons cons nil cons nil cons cons 443 remove subst 80 ref nil 129 ref 682 remove nil cons cons nil cons nil cons cons 133 ref subst nil 99 ref 196 ref nil cons 683 def cons 684 def 646 remove cons nil cons cons 685 def 116 ref subst 685 remove 170 ref subst nil 129 ref 55 ref nil cons 686 def cons nil cons nil cons cons 133 ref subst nil 684 remove 100 ref 686 remove cons 687 def nil cons cons nil cons cons 162 ref subst 80 ref 588 remove 55 ref appTerm absTerm 688 def 84 ref appTerm 689 def betaConv 52 ref 79 ref 688 ref appTerm 690 def absTerm 691 def 53 ref appTerm 692 def betaConv nil 202 ref 691 ref appTerm 693 def axiom nil 99 ref 693 remove nil cons cons 100 ref 692 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp 208 ref 209 ref 691 remove nil cons cons 212 ref cons nil cons cons 177 ref subst eqMp eqMp nil 99 ref 690 remove nil cons cons 100 ref 689 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp 607 ref 163 ref 688 remove nil cons cons 609 ref cons nil cons cons 177 ref subst eqMp eqMp eqMp eqMp eqMp nil 138 ref 683 remove cons 654 ref cons nil cons cons 153 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp eqMp eqMp nil 138 ref 641 ref cons 654 remove cons nil cons cons 153 ref subst deductAntisym eqMp nil 99 ref 33 ref 640 ref appTerm 694 def 644 remove appTerm nil cons cons 100 ref 13 ref 694 ref 55 remove appTerm appTerm 695 def 694 ref 121 ref appTerm appTerm nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp nil "q'" 3 ref var 696 def 121 ref nil cons cons nil cons nil cons cons 640 ref refl nil 99 ref 13 ref 640 ref appTerm 697 def 640 remove appTerm nil cons cons 100 ref 33 ref 694 ref 643 remove 696 ref varTerm 698 def appTerm 699 def appTerm appTerm 695 ref 694 remove 698 ref appTerm appTerm appTerm nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp nil "p'" 3 ref var 700 def 641 remove cons nil cons nil cons cons 696 ref 33 ref 697 remove 700 ref varTerm 701 def appTerm appTerm 33 ref 33 ref 701 ref appTerm 702 def 699 remove appTerm appTerm 695 remove 702 ref 698 ref appTerm 703 def appTerm appTerm appTerm absTerm 704 def 698 ref appTerm 705 def betaConv 700 ref 412 ref 704 ref appTerm 706 def absTerm 707 def 701 ref appTerm 708 def betaConv nil 687 remove 642 remove nil cons cons nil cons cons nil 415 ref 700 ref 412 ref 696 ref 33 ref 626 remove 701 ref appTerm 709 def appTerm 33 ref 702 ref 13 ref 103 ref appTerm 698 ref appTerm 710 def appTerm 711 def appTerm 105 remove 703 ref appTerm 712 def appTerm 713 def appTerm 714 def absTerm 715 def appTerm 716 def absTerm nil cons cons nil cons nil cons cons 597 ref subst 700 remove nil 129 ref 716 remove nil cons cons nil cons nil cons cons 133 ref subst nil 415 ref 715 remove nil cons cons nil cons nil cons cons 597 remove subst 696 remove nil 129 ref 714 remove nil cons cons nil cons nil cons cons 133 ref subst nil 99 ref 709 remove nil cons 717 def cons 718 def 100 ref 713 remove nil cons 719 def cons nil cons cons nil cons cons 720 def 116 ref subst 720 remove 170 ref subst nil 99 ref 711 ref nil cons 721 def cons 100 ref 712 remove nil cons 722 def cons nil cons cons nil cons cons 723 def 116 ref subst 723 remove 170 ref subst nil 661 ref 100 ref 703 ref nil cons 724 def cons nil cons cons nil cons cons 725 def 673 ref subst 725 ref 116 ref subst 725 remove 170 ref subst nil 99 ref 701 ref nil cons 726 def cons 727 def 100 ref 698 ref nil cons 728 def cons nil cons 729 def cons nil cons cons 730 def 116 ref subst 730 ref 170 ref subst nil 718 ref 100 ref 102 ref 701 remove appTerm 731 def nil cons 732 def cons nil cons cons nil cons cons 162 ref subst nil 99 ref 130 remove cons 100 ref 726 ref cons nil cons cons nil cons cons 733 def 637 ref subst eqMp 734 def nil 99 ref 732 ref cons 735 def 729 ref cons nil cons cons 736 def 162 ref subst proveHyp nil 718 remove 100 ref 702 remove 101 ref appTerm 737 def nil cons 738 def cons nil cons cons nil cons cons 162 ref subst 733 ref nil 629 remove 664 remove cons nil cons cons 739 def 116 ref subst 739 remove 170 ref subst 668 remove eqMp nil 635 remove 671 remove cons nil cons cons 153 ref subst deductAntisym eqMp 740 def subst eqMp 741 def nil 99 ref 738 ref cons 742 def 100 ref 33 ref 731 ref appTerm 743 def 698 ref appTerm nil cons 744 def cons nil cons cons nil cons cons 745 def 162 ref subst proveHyp 745 ref 116 ref subst 745 remove 170 ref subst 736 ref 116 ref subst 736 remove 170 ref subst nil 727 ref 669 remove cons nil cons cons 162 ref subst 737 remove assume eqMp 746 def 733 remove 162 ref subst 731 remove assume eqMp 747 def 746 remove proveHyp proveHyp nil 727 remove 100 ref 710 remove nil cons 748 def cons nil cons cons nil cons cons 162 ref subst 711 remove assume eqMp 749 def nil 99 ref 748 remove cons 750 def 100 ref 662 ref 698 ref appTerm 751 def nil cons 752 def cons nil cons cons nil cons cons 162 ref subst proveHyp nil 665 ref 729 ref cons nil cons cons 753 def 637 remove subst eqMp 754 def nil 99 ref 752 ref cons 755 def 729 remove cons nil cons cons 756 def 162 ref subst proveHyp 749 remove nil 750 remove 100 ref 33 ref 698 ref appTerm 103 ref appTerm 757 def nil cons 758 def cons nil cons cons nil cons cons 162 ref subst proveHyp 753 ref 740 remove subst eqMp 759 def nil 99 ref 758 ref cons 760 def 100 ref 33 ref 751 ref appTerm 761 def 698 remove appTerm nil cons 762 def cons nil cons cons nil cons cons 763 def 162 ref subst proveHyp 763 ref 116 ref subst 763 remove 170 ref subst 756 ref 116 ref subst 756 remove 170 ref subst 161 remove 753 remove 162 ref subst 751 remove assume eqMp proveHyp eqMp nil 138 ref 752 remove cons 764 def 140 ref 728 ref cons nil cons 765 def cons nil cons cons 153 ref subst deductAntisym eqMp eqMp nil 138 ref 758 remove cons 766 def 140 ref 762 remove cons nil cons cons nil cons cons 153 ref subst deductAntisym eqMp eqMp eqMp proveHyp eqMp nil 138 ref 732 remove cons 767 def 765 ref cons nil cons cons 153 ref subst deductAntisym eqMp eqMp nil 138 ref 738 remove cons 768 def 140 ref 744 remove cons nil cons cons nil cons cons 153 ref subst deductAntisym eqMp eqMp eqMp eqMp nil 138 ref 726 ref cons 765 remove cons nil cons cons 153 ref subst deductAntisym eqMp eqMp nil 670 ref 140 ref 724 ref cons nil cons cons nil cons cons 153 ref subst deductAntisym eqMp nil 99 ref 33 ref 104 ref appTerm 769 def 703 ref appTerm nil cons cons 100 ref 33 ref 703 ref appTerm 104 remove appTerm nil cons cons nil cons cons nil cons cons 170 ref subst proveHyp nil 99 ref 724 ref cons 631 remove cons nil cons cons 770 def 116 ref subst 770 remove 170 ref subst 116 ref 170 ref 734 remove nil 735 remove 666 ref cons nil cons cons 771 def 162 ref subst proveHyp 741 remove nil 742 remove 100 ref 743 remove 103 ref appTerm nil cons 772 def cons nil cons cons nil cons cons 773 def 162 ref subst proveHyp 773 ref 116 ref subst 773 remove 170 ref subst 771 ref 116 ref subst 771 remove 170 ref subst 747 remove 754 remove nil 755 remove 666 ref cons nil cons cons 774 def 162 ref subst proveHyp 759 remove nil 760 remove 100 ref 761 remove 103 remove appTerm nil cons 775 def cons nil cons cons nil cons cons 776 def 162 ref subst proveHyp 776 ref 116 ref subst 776 remove 170 ref subst 774 ref 116 ref subst 774 remove 170 ref subst 730 remove 162 ref subst 703 remove assume eqMp nil 99 ref 728 ref cons 666 remove cons nil cons cons 162 ref subst 757 remove assume eqMp proveHyp eqMp nil 764 remove 141 ref cons nil cons cons 153 ref subst deductAntisym eqMp eqMp nil 766 remove 140 ref 775 remove cons nil cons cons nil cons cons 153 ref subst deductAntisym eqMp eqMp eqMp proveHyp eqMp nil 767 remove 141 remove cons nil cons cons 153 ref subst deductAntisym eqMp eqMp nil 768 remove 140 ref 772 remove cons nil cons cons nil cons cons 153 ref subst deductAntisym eqMp eqMp eqMp eqMp 154 remove deductAntisym eqMp eqMp nil 138 ref 724 remove cons 636 remove cons nil cons cons 153 ref subst deductAntisym eqMp eqMp eqMp eqMp nil 138 ref 721 remove cons 140 ref 722 remove cons nil cons cons nil cons cons 153 ref subst deductAntisym eqMp eqMp nil 138 ref 717 remove cons 140 ref 719 remove cons nil cons cons nil cons cons 153 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp absThm eqMp subst nil 99 ref 412 ref 707 ref appTerm nil cons cons 100 ref 708 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp 414 ref 415 ref 707 remove nil cons cons 416 ref 726 remove cons nil cons cons nil cons cons 177 ref subst eqMp eqMp nil 99 ref 706 remove nil cons cons 100 ref 705 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp 414 ref 415 ref 704 remove nil cons cons 416 ref 728 remove cons nil cons cons nil cons cons 177 ref subst eqMp eqMp subst eqMp subst eqMp 653 remove 129 ref 13 ref 33 ref 131 ref appTerm 121 ref appTerm appTerm 121 ref appTerm absTerm 777 def 131 remove appTerm 778 def betaConv nil 412 ref 777 ref appTerm 779 def axiom nil 99 ref 779 remove nil cons cons 100 ref 778 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp 414 ref 415 ref 777 remove nil cons cons 417 remove cons nil cons cons 177 ref subst eqMp eqMp 780 def subst trans sym 132 ref eqMp 781 def subst eqMp eqMp nil 99 ref 79 ref 541 ref appTerm nil cons cons 100 ref 542 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp 607 ref 163 ref 541 remove nil cons cons 80 ref 463 ref nil cons cons nil cons 782 def cons nil cons cons 177 ref subst eqMp eqMp nil 99 ref 540 remove nil cons cons 100 ref 539 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp "A" 86 ref cons nil cons 783 def "P" 75 remove var 784 def 538 remove nil cons cons "x" 74 ref var 464 ref nil cons cons nil cons 785 def cons nil cons cons 177 ref subst eqMp eqMp sym subst 786 def appThm eqMp 453 ref 462 ref 341 ref 40 remove 1 ref 1 ref 1 ref 454 remove 86 ref cons opType 787 def 4 ref cons opType 788 def 787 ref nil cons 789 def cons opType constTerm "fn" 787 ref var 790 def 79 ref 460 ref 461 ref 462 ref 341 ref 790 ref varTerm 465 ref appTerm appTerm 791 def 464 ref appTerm absTerm appTerm absTerm appTerm absTerm 792 def appTerm 793 def 465 ref appTerm appTerm 464 ref appTerm absTerm 794 def 464 ref appTerm 795 def betaConv 460 ref 461 ref 794 ref appTerm 796 def absTerm 797 def 463 ref appTerm 798 def betaConv 792 ref 793 remove appTerm 799 def betaConv 49 remove 1 ref 788 ref 4 remove cons opType constTerm 800 def refl 790 remove 545 remove 460 ref 546 remove 462 ref 791 remove refl 460 ref 462 ref 464 ref absTerm 801 def absTerm 802 def 463 ref appTerm betaConv 549 remove appThm 801 remove 464 ref appTerm betaConv trans appThm absThm appThm absThm appThm absThm appThm "C" 86 ref cons nil cons "_1343" 1 ref 44 ref 1 ref 74 remove 86 remove cons opType nil cons cons opType var 802 remove nil cons cons nil cons nil cons cons 639 remove subst eqMp nil 99 ref 800 remove 792 ref appTerm nil cons cons 100 ref 799 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp "A" 789 remove cons nil cons "p" 788 remove var 792 remove nil cons cons nil cons nil cons cons 781 ref subst eqMp eqMp nil 99 ref 79 ref 797 ref appTerm nil cons cons 100 ref 798 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp 607 ref 163 ref 797 remove nil cons cons 782 ref cons nil cons cons 177 ref subst eqMp eqMp nil 99 ref 796 remove nil cons cons 100 ref 795 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp 783 ref 784 ref 794 remove nil cons cons 785 ref cons nil cons cons 177 ref subst eqMp eqMp sym subst 803 def appThm eqMp sym trans eqMp absThm eqMp eqMp absThm eqMp eqMp 441 ref 440 ref 478 ref nil cons 804 def cons "x" 257 ref var 805 def 496 remove nil cons cons nil cons cons nil cons cons 613 ref subst proveHyp nil 99 ref 387 ref 478 remove appTerm nil cons cons 100 ref 485 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp nil "p" 374 remove var 806 def 804 remove cons nil cons nil cons cons 442 remove 781 remove subst 807 def subst eqMp eqMp nil 99 ref 7 ref 483 ref appTerm nil cons cons 100 ref 484 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp 73 ref 237 ref 483 remove nil cons cons 238 ref 27 ref nil cons 808 def cons nil cons 809 def cons nil cons cons 177 ref subst eqMp eqMp nil 99 ref 482 remove nil cons cons 100 ref 481 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp 73 ref 237 ref 480 remove nil cons cons 238 ref 29 ref nil cons 810 def cons nil cons 811 def cons nil cons cons 177 ref subst eqMp eqMp trans 812 def appThm 448 remove betaConv 476 remove appThm 15 ref 279 ref 420 remove "_29352" 257 remove var 813 def 7 ref 9 ref 7 ref 15 ref 279 ref 813 remove varTerm 422 ref appTerm appTerm 291 ref 32 ref 297 ref 309 ref 446 ref 424 remove appTerm appTerm appTerm absTerm 313 ref appTerm 814 def appTerm 815 def appTerm absTerm appTerm absTerm appTerm absTerm 816 def appTerm 817 def 422 ref appTerm appTerm 815 ref appTerm absTerm 818 def 29 ref appTerm 819 def betaConv 9 ref 7 ref 818 ref appTerm 820 def absTerm 821 def 27 ref appTerm 822 def betaConv 816 ref 817 remove appTerm 823 def betaConv 816 ref "_29350" 246 ref var 824 def 284 ref 240 ref 490 remove 824 remove varTerm 825 def appTerm 826 def appTerm 285 ref appTerm appTerm 259 ref 493 remove 825 remove appTerm 827 def appTerm 289 ref appTerm appTerm 32 ref 292 ref 259 ref 826 ref appTerm 288 ref 270 ref 293 ref 827 ref appTerm 826 ref appTerm 828 def appTerm 287 ref appTerm appTerm appTerm appTerm 298 ref 299 ref 7 ref 60 ref 7 ref 253 ref 7 ref 254 ref 300 ref 301 ref 260 ref 303 ref 304 ref 268 ref 828 remove appTerm 302 ref appTerm appTerm appTerm appTerm absTerm 307 ref 268 ref 293 ref 826 ref appTerm 34 ref appTerm appTerm 263 ref appTerm appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 446 ref 423 ref 266 ref 826 ref appTerm 34 ref appTerm appTerm appTerm appTerm appTerm absTerm 266 ref 827 remove appTerm 826 remove appTerm appTerm appTerm absTerm 829 def appTerm betaConv sym nil 237 ref 9 ref 7 ref 15 ref 279 ref 829 ref 422 ref appTerm 830 def appTerm 815 ref appTerm 831 def absTerm 832 def appTerm 833 def absTerm nil cons cons nil cons nil cons cons 501 ref subst 9 ref nil 129 ref 833 remove nil cons cons nil cons nil cons cons 133 ref subst nil 237 ref 832 remove nil cons cons nil cons nil cons cons 501 ref subst 15 ref nil 129 ref 831 remove nil cons cons nil cons nil cons cons 133 ref subst 830 remove betaConv 279 ref "_29347" 2 ref var 834 def 284 ref 240 ref 834 ref varTerm 835 def appTerm 285 ref appTerm appTerm 836 def 290 ref appTerm 32 ref 292 ref 259 ref 835 ref appTerm 837 def 288 ref 270 ref 294 remove 835 ref appTerm 838 def appTerm 287 ref appTerm appTerm appTerm appTerm 298 ref 299 ref 7 ref 60 ref 7 ref 253 ref 7 ref 254 ref 300 ref 301 ref 260 ref 303 ref 304 ref 268 ref 838 remove appTerm 302 ref appTerm appTerm appTerm appTerm absTerm 307 ref 268 ref 293 ref 835 ref appTerm 34 ref appTerm appTerm 263 ref appTerm appTerm 839 def appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 446 ref 423 ref 266 ref 835 ref appTerm 34 ref appTerm appTerm appTerm 840 def appTerm appTerm absTerm 312 remove 835 ref appTerm appTerm appTerm absTerm 29 ref appTerm 841 def appTerm refl 834 ref 836 ref 511 remove appTerm 32 ref 292 ref 837 ref 288 ref 270 ref 512 remove 835 ref appTerm 842 def appTerm 287 ref appTerm appTerm appTerm appTerm 298 ref 299 ref 7 ref 60 ref 7 ref 253 ref 7 ref 254 ref 300 ref 301 ref 260 ref 303 ref 304 ref 268 ref 842 remove appTerm 302 ref appTerm appTerm appTerm appTerm absTerm 839 ref appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 840 ref appTerm appTerm absTerm 514 remove 835 ref appTerm appTerm appTerm absTerm 843 def 516 remove appTerm betaConv appThm 475 ref 841 remove betaConv appThm 517 remove 32 ref 519 remove 520 remove 446 ref 521 remove appTerm appTerm appTerm absTerm 522 remove appTerm appTerm refl appThm trans 523 remove "_29346" 2 ref var 844 def 834 remove 836 remove 259 remove 844 remove varTerm 845 def appTerm 289 remove appTerm appTerm 32 ref 292 remove 837 remove 288 remove 270 ref 293 remove 845 ref appTerm 835 ref appTerm 846 def appTerm 287 remove appTerm appTerm appTerm appTerm 298 ref 299 ref 7 ref 60 ref 7 ref 253 ref 7 ref 254 ref 300 ref 301 remove 260 ref 303 remove 304 ref 268 ref 846 remove appTerm 302 remove appTerm appTerm appTerm appTerm absTerm 839 remove appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 840 remove appTerm appTerm absTerm 266 ref 845 remove appTerm 835 remove appTerm appTerm appTerm absTerm absTerm 847 def 27 ref appTerm 848 def appTerm refl 847 ref 510 remove appTerm betaConv appThm 529 remove 848 remove betaConv appThm 843 remove refl appThm trans 847 remove refl 786 remove appThm eqMp 803 remove appThm eqMp sym trans eqMp absThm eqMp eqMp absThm eqMp eqMp 441 ref 440 ref 816 ref nil cons 849 def cons 805 ref 829 remove nil cons cons nil cons cons nil cons cons 613 ref subst proveHyp nil 99 ref 387 remove 816 remove appTerm nil cons cons 100 ref 823 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp nil 806 remove 849 remove cons nil cons nil cons cons 807 remove subst eqMp eqMp nil 99 ref 7 ref 821 ref appTerm nil cons cons 100 ref 822 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp 73 ref 237 ref 821 remove nil cons cons 809 remove cons nil cons cons 177 ref subst eqMp eqMp nil 99 ref 820 remove nil cons cons 100 ref 819 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp 73 ref 237 ref 818 remove nil cons cons 811 remove cons nil cons cons 177 ref subst eqMp eqMp trans appThm appThm absThm appThm absThm appThm trans sym nil 237 ref 9 ref 7 ref 15 ref 33 ref 7 ref 471 remove 7 ref 472 ref 33 ref 352 ref 474 ref appTerm 422 ref appTerm appTerm 279 ref 381 ref 474 ref appTerm appTerm 446 ref 474 remove appTerm appTerm appTerm absTerm appTerm absTerm 850 def appTerm 851 def appTerm 852 def 279 ref 426 ref appTerm 815 ref appTerm appTerm 853 def absTerm 854 def appTerm 855 def absTerm nil cons cons nil cons nil cons cons 501 ref subst 9 ref nil 129 ref 855 remove nil cons cons nil cons nil cons cons 133 ref subst nil 237 ref 854 remove nil cons cons nil cons nil cons cons 501 ref subst 15 ref nil 129 ref 853 remove nil cons cons nil cons nil cons cons 133 ref subst 14 ref "_29354" 249 ref var 856 def 852 ref 279 ref 856 remove varTerm appTerm 815 ref appTerm appTerm absTerm 857 def 426 ref appTerm betaConv appThm 17 ref 33 ref 286 ref appTerm 858 def refl 857 ref 290 ref appTerm betaConv appThm appThm 33 ref "Data.Bool.~" const 11 remove constTerm 859 def 286 ref appTerm 860 def appTerm 861 def refl 857 ref 425 ref appTerm betaConv appThm appThm appThm nil "_485" 249 ref var 862 def 425 ref nil cons cons "_482" 249 ref var 863 def 290 ref nil cons 864 def cons "_483" 3 ref var 865 def 286 ref nil cons 866 def cons nil cons cons cons nil cons cons nil "_484" 278 remove var 867 def 857 remove nil cons cons nil cons nil cons cons "A" 256 remove cons nil cons 43 remove cons 868 def nil 80 ref "_482" 44 ref var varTerm nil cons cons "c" 3 ref var 869 def 865 ref varTerm nil cons cons 52 ref "_484" 45 remove var varTerm nil cons cons "y" 44 ref var 870 def "_485" 44 ref var varTerm nil cons cons nil cons cons cons cons nil cons cons 870 ref 13 ref 53 ref 281 remove 1 ref 3 ref 1 ref 44 ref 1 ref 44 ref 54 remove cons opType nil cons cons opType nil cons cons opType constTerm 871 def 869 ref varTerm 872 def appTerm 84 ref appTerm 870 ref varTerm 873 def appTerm appTerm appTerm 16 ref 33 ref 872 ref appTerm 196 remove appTerm appTerm 33 ref 859 ref 872 ref appTerm appTerm 53 ref 873 ref appTerm appTerm appTerm appTerm absTerm 874 def 873 ref appTerm 875 def betaConv 80 ref 79 ref 874 ref appTerm 876 def absTerm 877 def 84 ref appTerm 878 def betaConv 869 remove 79 ref 877 ref appTerm 879 def absTerm 880 def 872 ref appTerm 881 def betaConv 52 remove 412 ref 880 ref appTerm 882 def absTerm 883 def 53 remove appTerm 884 def betaConv nil 202 remove 883 ref appTerm 885 def axiom nil 99 ref 885 remove nil cons cons 100 ref 884 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp 208 remove 209 remove 883 remove nil cons cons 212 remove cons nil cons cons 177 ref subst eqMp eqMp nil 99 ref 882 remove nil cons cons 100 ref 881 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp 414 ref 415 ref 880 remove nil cons cons 416 ref 872 remove nil cons cons nil cons cons nil cons cons 177 ref subst eqMp eqMp nil 99 ref 879 remove nil cons cons 100 ref 878 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp 607 ref 163 ref 877 remove nil cons cons 609 ref cons nil cons cons 177 ref subst eqMp eqMp nil 99 ref 876 remove nil cons cons 100 ref 875 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp 607 ref 163 ref 874 remove nil cons cons 80 ref 873 ref nil cons cons nil cons 886 def cons nil cons cons 177 ref subst eqMp eqMp subst subst 887 def subst subst eqMp sym nil 99 ref 866 ref cons 100 ref 852 ref 279 ref 290 ref appTerm 888 def 815 ref appTerm appTerm 889 def nil cons 890 def cons nil cons cons nil cons cons 891 def 116 ref subst 891 remove 170 ref subst 13 ref "_29356" 3 ref var 892 def 852 ref 888 ref 284 ref 892 remove varTerm appTerm 290 ref appTerm 814 ref appTerm appTerm appTerm absTerm 893 def 286 ref appTerm 894 def appTerm refl 893 ref 121 ref appTerm betaConv appThm 14 ref 894 remove betaConv appThm 852 ref 888 ref 284 ref 121 ref appTerm 895 def 290 ref appTerm 814 ref appTerm appTerm appTerm refl appThm trans 893 remove refl nil 129 ref 866 ref cons nil cons nil cons cons 133 ref subst 286 ref assume eqMp appThm eqMp sym 852 ref refl 896 def 888 remove refl nil "t2" 249 ref var 897 def 814 ref nil cons cons "t1" 249 ref var 898 def 864 ref cons nil cons cons nil cons cons 899 def 868 ref "t2" 44 ref var 900 def 530 ref 871 ref 121 ref appTerm "t1" 44 remove var 901 def varTerm 902 def appTerm 900 ref varTerm 903 def appTerm appTerm 902 ref appTerm absTerm 904 def 903 ref appTerm 905 def betaConv 901 ref 79 ref 904 ref appTerm 906 def absTerm 907 def 902 ref appTerm 908 def betaConv nil 79 ref 907 ref appTerm 909 def axiom nil 99 ref 909 remove nil cons cons 100 ref 908 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp 607 ref 163 ref 907 remove nil cons cons 80 ref 902 ref nil cons cons nil cons 910 def cons nil cons cons 177 ref subst eqMp eqMp nil 99 ref 906 remove nil cons cons 100 ref 905 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp 607 ref 163 ref 904 remove nil cons cons 80 ref 903 ref nil cons cons nil cons 911 def cons nil cons cons 177 ref subst eqMp eqMp subst 912 def subst appThm nil "x" 249 ref var 913 def 864 remove cons nil cons nil cons cons 868 ref nil 129 ref 530 ref 84 ref appTerm 84 ref appTerm nil cons cons nil cons nil cons cons 133 ref subst 176 remove eqMp subst 914 def subst trans appThm nil 129 ref 851 remove nil cons 915 def cons nil cons nil cons cons 780 remove subst 916 def trans sym 132 ref eqMp eqMp eqMp nil 138 ref 866 remove cons 917 def 140 ref 890 remove cons nil cons cons nil cons cons 153 ref subst deductAntisym eqMp nil 99 ref 858 remove 889 remove appTerm nil cons cons 100 ref 861 remove 852 ref 279 ref 425 ref appTerm 918 def 815 remove appTerm appTerm 919 def appTerm nil cons cons nil cons cons nil cons cons 170 ref subst proveHyp nil 99 ref 860 remove nil cons 920 def cons 921 def 100 ref 919 remove nil cons 922 def cons nil cons cons nil cons cons 923 def 116 ref subst 923 remove 170 ref subst 13 ref "_29358" 3 ref var 924 def 852 ref 918 ref 284 ref 924 remove varTerm appTerm 290 ref appTerm 814 ref appTerm appTerm appTerm absTerm 925 def 286 ref appTerm 926 def appTerm refl 925 ref "Data.Bool.F" const 3 ref constTerm 927 def appTerm betaConv appThm 14 ref 926 remove betaConv appThm 852 ref 918 remove 284 ref 927 ref appTerm 928 def 290 remove appTerm 814 ref appTerm appTerm appTerm refl appThm trans 925 remove refl nil 921 ref 100 ref 13 ref 286 remove appTerm 927 ref appTerm nil cons cons nil cons cons nil cons cons 162 ref subst nil 917 remove nil cons nil cons cons nil 99 ref 859 ref 142 ref appTerm 929 def nil cons 930 def cons 100 ref 13 ref 142 ref appTerm 927 ref appTerm nil cons 931 def cons nil cons cons nil cons cons 932 def 116 ref subst 932 remove 170 ref subst nil 99 ref 142 ref nil cons 933 def cons 100 ref 927 ref nil cons 934 def cons nil cons cons nil cons cons 673 remove subst 13 ref 929 ref appTerm refl 99 ref 102 remove 927 ref appTerm absTerm 935 def 142 ref appTerm betaConv appThm nil 125 remove 859 ref appTerm 935 remove appTerm axiom 151 remove appThm eqMp 929 remove assume eqMp nil 99 ref 33 ref 142 ref appTerm 927 ref appTerm nil cons cons 100 ref 33 ref 927 ref appTerm 142 ref appTerm nil cons cons nil cons cons nil cons cons 170 ref subst proveHyp nil 99 ref 934 ref cons 100 ref 933 ref cons nil cons cons nil cons cons 936 def 116 ref subst 936 remove 170 ref subst 99 ref 101 remove absTerm 937 def 142 remove appTerm 938 def betaConv nil 13 ref 927 ref appTerm 412 remove 937 ref appTerm 939 def appTerm axiom 927 ref assume eqMp nil 99 ref 939 remove nil cons cons 100 ref 938 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp 414 remove 415 remove 937 remove nil cons cons 416 remove 933 ref cons nil cons cons nil cons cons 177 ref subst eqMp eqMp eqMp nil 138 ref 934 remove cons 140 ref 933 remove cons nil cons cons nil cons cons 153 ref subst deductAntisym eqMp eqMp eqMp eqMp nil 138 ref 930 remove cons 140 ref 931 remove cons nil cons cons nil cons cons 153 ref subst deductAntisym eqMp 940 def subst eqMp appThm eqMp sym 896 ref 475 ref 425 remove betaConv 284 ref 240 ref 313 ref appTerm 285 ref appTerm 941 def appTerm 296 ref appTerm 942 def refl 943 def 298 ref refl 299 ref 8 ref 60 ref 8 ref 253 ref 8 remove 254 ref 300 ref refl 306 remove 307 remove 268 ref 308 remove 313 ref appTerm appTerm 263 ref appTerm appTerm 944 def appTerm betaConv appThm absThm appThm absThm appThm absThm appThm absThm appThm 945 def 381 ref 261 ref 313 ref appTerm 946 def 310 remove 313 ref appTerm 947 def appTerm 948 def appTerm 949 def refl appThm appThm trans appThm 899 remove 868 remove 900 remove 530 remove 871 remove 927 ref appTerm 902 ref appTerm 903 ref appTerm appTerm 903 ref appTerm absTerm 950 def 903 remove appTerm 951 def betaConv 901 remove 79 ref 950 ref appTerm 952 def absTerm 953 def 902 remove appTerm 954 def betaConv nil 79 ref 953 ref appTerm 955 def axiom nil 99 ref 955 remove nil cons cons 100 ref 954 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp 607 ref 163 ref 953 remove nil cons cons 910 remove cons nil cons cons 177 ref subst eqMp eqMp nil 99 ref 952 remove nil cons cons 100 ref 951 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp 607 ref 163 ref 950 remove nil cons cons 911 remove cons nil cons cons 177 ref subst eqMp eqMp subst 956 def subst 814 remove betaConv trans 943 remove 945 remove 446 ref 948 ref appTerm 957 def refl appThm appThm trans appThm appThm sym 14 ref "_29360" 249 ref var 958 def 852 ref 279 ref 958 remove varTerm appTerm 942 ref 298 remove 299 remove 7 ref 60 ref 7 ref 253 ref 7 ref 254 ref 300 remove 260 remove 261 remove 944 ref appTerm 304 remove 305 remove 944 remove appTerm appTerm appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 959 def 957 ref appTerm 960 def appTerm 961 def appTerm appTerm absTerm 962 def 942 remove 959 ref 949 ref appTerm 963 def appTerm appTerm betaConv appThm 17 remove 33 ref 941 ref appTerm 964 def refl 962 ref 296 ref appTerm betaConv appThm appThm 33 ref 859 ref 941 ref appTerm 965 def appTerm 966 def refl 962 ref 963 ref appTerm betaConv appThm appThm appThm nil 862 remove 963 ref nil cons 967 def cons 863 remove 296 ref nil cons 968 def cons 865 remove 941 ref nil cons 969 def cons nil cons cons cons nil cons cons nil 867 remove 962 remove nil cons cons nil cons nil cons cons 887 remove subst subst eqMp sym nil 99 ref 969 ref cons 100 ref 852 ref 279 ref 296 ref appTerm 970 def 961 ref appTerm appTerm 971 def nil cons 972 def cons nil cons cons nil cons cons 973 def 116 ref subst 973 remove 170 ref subst 13 ref "_29362" 3 ref var 974 def 852 ref 970 ref 284 ref 974 remove varTerm appTerm 296 ref appTerm 960 ref appTerm appTerm appTerm absTerm 975 def 941 ref appTerm 976 def appTerm refl 975 ref 121 remove appTerm betaConv appThm 14 ref 976 remove betaConv appThm 852 ref 970 ref 895 remove 296 ref appTerm 960 ref appTerm appTerm appTerm refl appThm trans 975 remove refl nil 129 ref 969 ref cons nil cons nil cons cons 133 ref subst 941 ref assume eqMp appThm eqMp sym 896 remove 970 remove refl nil 897 ref 960 ref nil cons cons 898 remove 968 ref cons nil cons 977 def cons nil cons cons 912 remove subst appThm nil 913 ref 968 remove cons nil cons nil cons cons 914 ref subst trans appThm 916 remove trans sym 132 ref eqMp eqMp eqMp nil 138 ref 969 remove cons 978 def 140 ref 972 remove cons nil cons cons nil cons cons 153 ref subst deductAntisym eqMp nil 99 ref 964 remove 971 remove appTerm nil cons cons 100 ref 966 remove 852 ref 279 ref 963 ref appTerm 979 def 961 remove appTerm appTerm 980 def appTerm nil cons cons nil cons cons nil cons cons 170 ref subst proveHyp nil 99 ref 965 remove nil cons 981 def cons 982 def 100 ref 980 remove nil cons 983 def cons nil cons cons nil cons cons 984 def 116 ref subst 984 remove 170 ref subst 13 ref "_29364" 3 ref var 985 def 852 ref 979 ref 284 remove 985 remove varTerm appTerm 296 ref appTerm 960 ref appTerm appTerm appTerm absTerm 986 def 941 ref appTerm 987 def appTerm refl 986 ref 927 ref appTerm betaConv appThm 14 ref 987 remove betaConv appThm 852 remove 979 ref 928 remove 296 remove appTerm 988 def 960 remove appTerm appTerm 989 def appTerm refl appThm trans 986 remove refl nil 982 ref 100 ref 13 ref 941 remove appTerm 927 remove appTerm nil cons cons nil cons cons nil cons cons 162 ref subst nil 978 remove nil cons nil cons cons 940 remove subst eqMp appThm eqMp sym nil 99 ref 915 ref cons 990 def 100 ref 989 ref nil cons 991 def cons nil cons 992 def cons nil cons cons 993 def 116 ref subst 993 remove 170 ref subst 472 remove 33 ref 352 ref 946 remove 473 remove appTerm 994 def appTerm 422 ref appTerm appTerm 279 ref 381 ref 994 ref appTerm appTerm 446 remove 994 remove appTerm appTerm appTerm absTerm 995 def 947 ref appTerm 996 def betaConv 850 ref 313 ref appTerm 997 def betaConv nil 990 remove 100 ref 997 remove nil cons cons nil cons cons nil cons cons 162 ref subst 73 ref 237 ref 850 remove nil cons cons 238 ref 313 ref nil cons 998 def cons nil cons 999 def cons nil cons cons 177 ref subst eqMp eqMp nil 99 ref 7 ref 995 ref appTerm nil cons cons 100 ref 996 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp 73 ref 237 ref 995 remove nil cons cons 238 ref 947 ref nil cons 1000 def cons nil cons cons nil cons cons 177 ref subst eqMp eqMp nil 99 ref 33 ref 352 remove 948 ref appTerm 422 ref appTerm 1001 def appTerm 279 ref 949 ref appTerm 957 ref appTerm 1002 def appTerm 1003 def nil cons cons 992 ref cons nil cons cons 162 ref subst proveHyp nil "y" 246 remove var 422 ref nil cons 1004 def cons 337 ref 948 remove nil cons cons 395 remove cons cons nil cons cons 355 remove 870 remove 13 ref 399 remove 84 ref appTerm 873 ref appTerm appTerm "Number.Natural.<" const 18 remove constTerm 1005 def 398 ref 84 ref appTerm appTerm 398 ref 873 ref appTerm appTerm appTerm absTerm 1006 def 873 remove appTerm 1007 def betaConv 80 remove 79 ref 1006 ref appTerm 1008 def absTerm 1009 def 84 remove appTerm 1010 def betaConv 397 remove 79 ref 1009 ref appTerm 1011 def absTerm 1012 def 398 remove appTerm 1013 def betaConv nil 404 remove 1012 ref appTerm 1014 def axiom nil 99 ref 1014 remove nil cons cons 100 ref 1013 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp 406 remove 407 remove 1012 remove nil cons cons 408 remove cons nil cons cons 177 ref subst eqMp eqMp nil 99 ref 1011 remove nil cons cons 100 ref 1010 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp 607 ref 163 ref 1009 remove nil cons cons 609 remove cons nil cons cons 177 ref subst eqMp eqMp nil 99 ref 1008 remove nil cons cons 100 ref 1007 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp 607 ref 163 ref 1006 remove nil cons cons 886 remove cons nil cons cons 177 ref subst eqMp eqMp subst subst 1005 ref refl nil 15 ref 1000 ref cons 9 ref 998 ref cons nil cons cons nil cons cons 453 remove 462 remove 341 remove 350 remove 787 remove constTerm 465 remove appTerm appTerm 464 ref appTerm absTerm 1015 def 464 remove appTerm 1016 def betaConv 460 remove 461 remove 1015 ref appTerm 1017 def absTerm 1018 def 463 remove appTerm 1019 def betaConv nil 79 remove 1018 ref appTerm 1020 def axiom nil 99 ref 1020 remove nil cons cons 100 ref 1019 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp 607 remove 163 remove 1018 remove nil cons cons 782 remove cons nil cons cons 177 ref subst eqMp eqMp nil 99 ref 1017 remove nil cons cons 100 ref 1016 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp 783 remove 784 remove 1015 remove nil cons cons 785 remove cons nil cons cons 177 ref subst eqMp eqMp subst 1021 def subst appThm 1021 remove appThm trans sym "n" 2 ref var 1022 def 16 ref 1005 ref 947 remove appTerm 1023 def 1022 ref varTerm 1024 def appTerm appTerm 1005 ref 1024 ref appTerm 1025 def 29 ref appTerm appTerm absTerm 1026 def 313 ref appTerm betaConv sym nil 982 remove 100 ref 1023 ref 313 ref appTerm nil cons 1027 def cons nil cons cons nil cons cons 162 ref subst nil 1022 ref 998 remove cons "m" 2 ref var 1028 def 810 ref cons nil cons cons nil cons cons 1022 ref 33 ref 859 remove 240 ref 1024 ref appTerm 285 remove appTerm appTerm appTerm 1005 ref 266 ref 1028 ref varTerm 1029 def appTerm 1024 ref appTerm appTerm 1024 ref appTerm appTerm absTerm 1030 def 1024 ref appTerm 1031 def betaConv 1028 ref 7 ref 1030 ref appTerm 1032 def absTerm 1033 def 1029 ref appTerm 1034 def betaConv nil 7 ref 1033 ref appTerm 1035 def axiom nil 99 ref 1035 remove nil cons cons 100 ref 1034 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp 73 ref 237 ref 1033 remove nil cons cons 238 ref 1029 ref nil cons cons nil cons 1036 def cons nil cons cons 177 ref subst eqMp eqMp nil 99 ref 1032 remove nil cons cons 100 ref 1031 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp 73 ref 237 ref 1030 remove nil cons cons 238 ref 1024 ref nil cons cons nil cons 1037 def cons nil cons cons 177 ref subst eqMp eqMp 1038 def subst eqMp nil 99 ref 1027 remove cons 100 ref 1005 ref 313 ref appTerm 29 ref appTerm nil cons cons nil cons 1039 def cons nil cons cons 170 ref subst proveHyp nil 921 remove 1039 remove cons nil cons cons 162 ref subst nil 1022 ref 810 ref cons 1028 ref 808 remove cons nil cons cons nil cons cons 1038 remove subst eqMp eqMp eqMp 73 ref 237 ref 1026 ref nil cons cons 999 remove cons nil cons cons 613 ref subst proveHyp nil 99 ref 59 ref 1026 remove appTerm nil cons cons 100 ref 1023 remove 29 ref appTerm nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp nil "p" 2 ref var 1040 def 810 remove cons 1028 ref 1000 remove cons nil cons cons nil cons cons 1040 ref 33 ref 59 remove 1022 ref 16 ref 1005 remove 1029 ref appTerm 1041 def 1024 ref appTerm appTerm 1025 remove 1040 ref varTerm 1042 def appTerm appTerm 1043 def absTerm 1044 def appTerm 1045 def appTerm 1046 def 1041 remove 1042 ref appTerm 1047 def appTerm 1048 def absTerm 1049 def 1042 ref appTerm 1050 def betaConv 1028 ref 7 ref 1049 ref appTerm 1051 def absTerm 1052 def 1029 ref appTerm 1053 def betaConv nil 7 ref 1028 ref 7 ref 1022 ref 7 ref 1040 ref 33 ref 1043 ref appTerm 1047 ref appTerm absTerm 1054 def appTerm 1055 def absTerm 1056 def appTerm 1057 def absTerm 1058 def appTerm 1059 def axiom nil 99 ref 1059 ref nil cons 1060 def cons 1061 def 100 ref 7 ref 1052 ref appTerm nil cons 1062 def cons nil cons cons nil cons cons 1063 def 162 ref subst proveHyp 1063 ref 116 ref subst 1063 remove 170 ref subst nil 237 ref 1052 remove nil cons cons 1064 def nil cons nil cons cons 501 ref subst 1028 remove nil 129 ref 1051 remove nil cons 1065 def cons nil cons nil cons cons 133 ref subst nil 237 ref 1049 remove nil cons cons 1066 def nil cons nil cons cons 501 ref subst 1040 remove nil 129 ref 1048 remove nil cons cons nil cons nil cons cons 133 ref subst nil 99 ref 1045 remove nil cons 1067 def cons 1068 def 100 ref 1047 ref nil cons 1069 def cons nil cons 1070 def cons nil cons cons 1071 def 116 ref subst 1071 remove 170 ref subst nil 1061 ref 1070 ref cons nil cons cons 1072 def 162 ref subst nil 1068 remove 100 ref 33 ref 1059 remove appTerm 1047 remove appTerm 1073 def nil cons 1074 def cons nil cons 1075 def cons nil cons cons 162 ref subst nil 237 ref 1022 ref 33 ref 1044 ref 1024 ref appTerm 1076 def appTerm 1073 ref appTerm 1077 def absTerm nil cons cons nil cons nil cons cons 501 ref subst 1022 remove nil 129 ref 1077 remove nil cons cons nil cons nil cons cons 133 ref subst nil 99 ref 1076 ref nil cons 1078 def cons 1075 ref cons nil cons cons 1079 def 116 ref subst 1079 remove 170 ref subst 1076 ref betaConv 1076 remove assume eqMp nil 99 ref 1043 remove nil cons 1080 def cons 1081 def 1075 remove cons nil cons cons 1082 def 162 ref subst proveHyp 1082 ref 116 ref subst 1082 remove 170 ref subst 1072 ref 116 ref subst 1072 remove 170 ref subst nil 1081 remove 1070 remove cons nil cons cons 162 ref subst 1054 ref 1042 ref appTerm 1083 def betaConv 1056 ref 1024 remove appTerm 1084 def betaConv 1058 ref 1029 remove appTerm 1085 def betaConv nil 1061 remove 100 ref 1085 remove nil cons cons nil cons cons nil cons cons 162 ref subst 73 ref 237 ref 1058 remove nil cons cons 1036 ref cons nil cons cons 177 ref subst eqMp eqMp nil 99 ref 1057 remove nil cons cons 100 ref 1084 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp 73 ref 237 ref 1056 remove nil cons cons 1037 remove cons nil cons cons 177 ref subst eqMp eqMp nil 99 ref 1055 remove nil cons cons 100 ref 1083 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp 73 ref 237 ref 1054 remove nil cons cons 238 ref 1042 remove nil cons cons nil cons 1086 def cons nil cons cons 177 ref subst eqMp eqMp eqMp eqMp nil 138 ref 1060 remove cons 1087 def 140 ref 1069 remove cons nil cons 1088 def cons nil cons cons 153 ref subst deductAntisym eqMp eqMp nil 138 ref 1080 remove cons 140 ref 1074 remove cons nil cons 1089 def cons nil cons cons 153 ref subst deductAntisym eqMp eqMp eqMp nil 138 ref 1078 remove cons 1089 ref cons nil cons cons 153 ref subst deductAntisym eqMp eqMp absThm eqMp nil 99 ref 7 ref 238 ref 33 ref 1044 ref 238 remove varTerm 1090 def appTerm appTerm 1073 ref appTerm absTerm appTerm nil cons cons 100 ref 1046 remove 1073 remove appTerm nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp 73 ref 237 ref 1044 remove nil cons cons 1089 remove cons nil cons cons 638 ref subst eqMp eqMp eqMp eqMp nil 138 ref 1067 remove cons 1088 remove cons nil cons cons 153 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp nil 1087 remove 140 ref 1062 ref cons nil cons cons nil cons cons 153 ref subst deductAntisym eqMp eqMp nil 99 ref 1062 remove cons 100 ref 1053 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp 73 ref 1064 remove 1036 remove cons nil cons cons 177 ref subst eqMp eqMp nil 99 ref 1065 remove cons 100 ref 1050 remove nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp 73 remove 1066 remove 1086 remove cons nil cons cons 177 ref subst eqMp eqMp subst eqMp eqMp nil 99 ref 1001 ref nil cons cons 1091 def 100 ref 33 ref 1002 ref appTerm 989 ref appTerm 1092 def nil cons cons nil cons cons nil cons cons 170 ref subst proveHyp nil 99 ref 1002 ref nil cons 1093 def cons 992 remove cons nil cons cons 1094 def 116 ref subst 1094 remove 170 ref subst 13 remove "_29366" 249 remove var 1095 def 979 ref 988 ref 959 remove 1095 remove varTerm appTerm appTerm appTerm absTerm 1096 def 957 remove appTerm 1097 def appTerm refl 1096 ref 949 remove appTerm betaConv appThm 14 remove 1097 remove betaConv appThm 979 ref 988 remove 963 remove appTerm appTerm refl appThm trans 1096 remove refl 1002 remove assume sym appThm eqMp sym 979 remove refl nil 897 remove 967 ref cons 977 remove cons nil cons cons 956 remove subst appThm nil 913 remove 967 remove cons nil cons nil cons cons 914 remove subst trans sym 132 remove eqMp eqMp eqMp nil 138 ref 1093 ref cons 140 ref 991 ref cons nil cons 1098 def cons nil cons cons 153 ref subst deductAntisym eqMp eqMp nil 99 ref 16 ref 1001 remove appTerm 1092 remove appTerm nil cons cons 100 ref 33 ref 1003 remove appTerm 989 remove appTerm nil cons cons nil cons cons nil cons cons 162 ref subst proveHyp nil "r" 3 remove var 1099 def 991 remove cons 100 ref 1093 remove cons 1091 remove nil cons cons cons nil cons cons nil 99 ref 106 remove 662 remove 1099 ref varTerm 1100 def appTerm 1101 def appTerm nil cons 1102 def cons 100 ref 769 remove 1100 ref appTerm nil cons 1103 def cons nil cons cons nil cons cons 1104 def 116 ref subst 1104 remove 170 ref subst nil 661 remove 100 ref 1100 remove nil cons 1105 def cons nil cons 1106 def cons nil cons cons 1107 def 116 ref subst 1107 remove 170 ref subst nil 139 remove 140 ref 1101 remove nil cons cons nil cons cons nil cons cons 1108 def 153 ref subst 162 ref proveHyp 155 remove eqMp nil 665 remove 1106 remove cons nil cons cons 162 ref subst proveHyp 1108 remove 234 remove subst eqMp eqMp nil 670 remove 140 ref 1105 remove cons nil cons cons nil cons cons 153 ref subst deductAntisym eqMp eqMp nil 138 ref 1102 remove cons 140 ref 1103 remove cons nil cons cons nil cons cons 153 ref subst deductAntisym eqMp 1109 def subst eqMp eqMp eqMp nil 138 ref 915 remove cons 1098 remove cons nil cons cons 153 ref subst deductAntisym eqMp eqMp eqMp nil 138 ref 981 remove cons 140 ref 983 remove cons nil cons cons nil cons cons 153 ref subst deductAntisym eqMp eqMp eqMp eqMp eqMp eqMp nil 138 ref 920 remove cons 140 ref 922 remove cons nil cons cons nil cons cons 153 ref subst deductAntisym eqMp eqMp eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp eqMp absThm eqMp eqMp absThm eqMp nil 99 ref 434 ref nil cons cons 1110 def 100 ref 33 ref 438 ref appTerm 391 ref appTerm 1111 def nil cons cons nil cons 1112 def cons nil cons cons 170 ref subst proveHyp nil 440 ref 377 ref 33 ref 437 ref 381 ref appTerm 1113 def appTerm 391 ref appTerm 1114 def absTerm nil cons cons nil cons nil cons cons 444 remove subst 377 remove nil 129 ref 1114 remove nil cons cons nil cons nil cons cons 133 ref subst nil 99 ref 1113 ref nil cons 1115 def cons 393 ref cons nil cons cons 1116 def 116 ref subst 1116 remove 170 ref subst 1113 ref betaConv 1113 remove assume eqMp nil 99 ref 436 remove nil cons 1117 def cons 1118 def 393 remove cons nil cons cons 1119 def 162 ref subst proveHyp 1119 ref 116 remove subst 1119 remove 170 remove subst 314 ref 9 ref 15 ref 381 ref 422 remove appTerm absTerm 1120 def absTerm 1121 def appTerm betaConv sym nil 237 ref 9 ref 7 ref 15 ref 279 ref 1121 ref 27 ref appTerm 1122 def 29 ref appTerm appTerm 291 ref 32 ref 297 ref 309 ref 1121 ref 34 ref appTerm 1123 def 311 ref appTerm appTerm appTerm absTerm 313 ref appTerm appTerm appTerm 1124 def absTerm 1125 def appTerm 1126 def absTerm nil cons cons nil cons nil cons cons 501 ref subst 9 ref nil 129 ref 1126 remove nil cons cons nil cons nil cons cons 133 ref subst nil 237 ref 1125 remove nil cons cons nil cons nil cons cons 501 ref subst 15 ref nil 129 ref 1124 remove nil cons cons nil cons nil cons cons 133 ref subst 475 ref 1122 remove betaConv 29 ref refl appThm 1120 remove 29 ref appTerm betaConv trans appThm 291 ref refl 32 ref 297 ref refl 309 ref refl 1123 remove betaConv 311 ref refl appThm 15 ref 381 remove 423 remove 29 ref appTerm appTerm absTerm 311 ref appTerm betaConv trans appThm appThm absThm 313 ref refl appThm appThm appThm sym 475 remove nil 337 ref 1004 remove cons nil cons nil cons cons 435 ref 340 ref appTerm 1127 def betaConv nil 1118 remove 100 ref 1127 remove nil cons cons nil cons cons nil cons cons 162 ref subst 354 remove "P" 322 remove var 435 remove nil cons cons 337 remove 340 remove nil cons cons nil cons cons nil cons cons 177 remove subst eqMp eqMp subst appThm 426 remove refl appThm sym 812 remove eqMp eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp 319 remove "P" 316 remove var 314 remove nil cons cons "x" 276 ref var 1121 remove nil cons cons nil cons cons nil cons cons 613 remove subst proveHyp eqMp nil 138 ref 1117 remove cons 140 remove 392 ref cons nil cons 1128 def cons nil cons cons 153 ref subst deductAntisym eqMp eqMp eqMp nil 138 ref 1115 remove cons 1128 ref cons nil cons cons 153 ref subst deductAntisym eqMp eqMp absThm eqMp nil 99 ref 376 remove 805 ref 33 ref 437 ref 805 remove varTerm appTerm appTerm 391 ref appTerm absTerm appTerm nil cons cons 1112 remove cons nil cons cons 162 ref subst proveHyp 441 remove 440 remove 437 remove nil cons cons 1128 ref cons nil cons cons 638 remove subst eqMp eqMp nil 99 remove 16 remove 434 remove appTerm 1111 remove appTerm nil cons cons 100 ref 33 remove 439 remove appTerm 391 remove appTerm nil cons cons nil cons cons nil cons cons 162 remove subst proveHyp nil 1099 remove 392 remove cons 100 remove 438 remove nil cons cons 1110 remove nil cons cons cons nil cons cons 1109 remove subst eqMp eqMp eqMp nil 138 remove 409 remove cons 1128 remove cons nil cons cons 153 remove subst deductAntisym eqMp eqMp eqMp eqMp eqMp defineConstList 1129 def pop hdTl pop 276 remove constTerm 1130 def 271 ref appTerm 272 ref appTerm appTerm 1131 def absTerm 1132 def absTerm 1133 def absTerm 1134 def absTerm 1135 def defineConst 1136 def pop 1 ref 2 ref 1 remove 2 remove 41 remove cons opType nil cons cons opType constTerm 1137 def 27 ref appTerm 29 ref appTerm 1090 ref appTerm 239 remove varTerm 1138 def appTerm appTerm 251 remove 252 remove 7 ref 60 remove 7 ref 253 remove 7 ref 254 remove 265 remove 266 remove 267 remove 268 ref 1090 remove appTerm 268 ref 270 remove 27 ref appTerm 263 remove appTerm appTerm 29 ref appTerm appTerm appTerm 268 ref 1138 remove appTerm 274 remove 27 ref appTerm appTerm appTerm appTerm 268 remove 27 ref appTerm 29 ref appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 1130 ref 27 remove appTerm 29 remove appTerm 1139 def appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm 1140 def nil cons cons nil cons nil cons cons 501 ref subst 241 remove nil 129 ref 7 ref 242 ref 7 ref 243 ref 7 ref 244 ref 240 remove 1137 remove 271 ref appTerm 272 ref appTerm 269 ref appTerm 273 ref appTerm appTerm 1131 remove appTerm 1141 def absTerm 1142 def appTerm 1143 def absTerm 1144 def appTerm 1145 def absTerm 1146 def appTerm nil cons cons nil cons nil cons cons 133 ref subst nil 237 ref 1146 remove nil cons cons nil cons nil cons cons 501 ref subst 242 remove nil 129 ref 1145 remove nil cons cons nil cons nil cons cons 133 ref subst nil 237 ref 1144 remove nil cons cons nil cons nil cons cons 501 ref subst 243 remove nil 129 ref 1143 remove nil cons cons nil cons nil cons cons 133 ref subst nil 237 remove 1142 remove nil cons cons nil cons nil cons cons 501 remove subst 244 remove nil 129 remove 1141 remove nil cons cons nil cons nil cons cons 133 remove subst 1136 remove 271 ref refl appThm 1135 remove 271 remove appTerm betaConv trans 272 ref refl appThm 1134 remove 272 remove appTerm betaConv trans 269 ref refl appThm 1133 remove 269 remove appTerm betaConv trans 273 ref refl appThm 1132 remove 273 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp nil 7 ref 1140 remove appTerm thm 1129 remove nil 7 ref 9 remove 7 remove 15 remove 279 remove 1139 remove appTerm 291 remove 32 remove 297 remove 309 remove 1130 remove 34 remove appTerm 311 remove appTerm appTerm appTerm absTerm 313 remove appTerm appTerm appTerm absTerm appTerm absTerm appTerm thm