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