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