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