path: "vendor/opentheory/data/theories/natural-exp-def/natural-exp-def.art"
6 version "Number.Natural.^" "EXP" "->" typeOp 0 def "Number.Natural.natural" typeOp nil opType 1 def 0 ref 1 ref 1 ref nil cons 2 def cons opType 3 def nil cons 4 def cons opType 5 def var 6 def nil cons cons nil cons 6 ref "Data.Bool./\\" const 0 ref "bool" typeOp nil opType 7 def 0 ref 7 ref 7 ref nil cons 8 def cons opType 9 def nil cons cons opType 10 def constTerm 11 def "Data.Bool.!" const 12 def 0 ref 0 ref 1 ref 8 ref cons opType 13 def 8 ref cons opType constTerm 14 def "m" 1 ref var 15 def "=" const 16 def 0 ref 1 ref 13 ref nil cons cons opType constTerm 17 def 6 ref varTerm 18 def 15 ref varTerm 19 def appTerm 20 def "Number.Natural.zero" const 1 ref constTerm 21 def appTerm appTerm "Number.Natural.bit1" const 3 ref constTerm 21 ref appTerm 22 def appTerm absTerm appTerm appTerm 14 ref 15 ref 14 ref "n" 1 ref var 23 def 17 ref 20 ref "Number.Natural.suc" const 3 ref constTerm 23 ref varTerm 24 def appTerm 25 def appTerm appTerm "Number.Natural.*" const 5 ref constTerm 19 ref appTerm 26 def 20 remove 24 ref appTerm appTerm appTerm absTerm appTerm absTerm appTerm appTerm absTerm 27 def refl 28 def 16 ref 0 ref 5 ref 0 ref 5 ref 8 ref cons opType 29 def nil cons cons opType constTerm 30 def 18 ref appTerm 31 def "select" const 32 def 0 ref 29 ref 5 ref nil cons 33 def cons opType constTerm 34 def 27 ref appTerm appTerm assume sym appThm 27 ref 18 ref appTerm betaConv 35 def trans "A" 33 ref cons nil cons 36 def nil nil cons 37 def cons 38 def nil 16 ref 0 ref 0 ref 0 ref "A" varType 39 def 8 ref cons opType 40 def 8 ref cons opType 41 def 0 ref 41 ref 8 ref cons opType nil cons cons opType constTerm 42 def "Data.Bool.?" const 43 def 41 ref constTerm 44 def appTerm 45 def "p" 40 ref var 46 def 46 ref varTerm 47 def 32 remove 0 ref 40 ref 39 ref nil cons 48 def cons opType constTerm 47 ref appTerm appTerm absTerm appTerm axiom subst 28 remove appThm "p" 29 ref var 49 def 49 remove varTerm 50 def 34 remove 50 remove appTerm appTerm absTerm 27 ref appTerm betaConv trans 43 ref 0 ref 29 ref 8 ref cons opType 51 def constTerm 52 def refl "fn" 5 ref var 53 def 11 ref 16 ref 0 ref 3 ref 0 ref 3 ref 8 ref cons opType nil cons cons opType constTerm 54 def 53 remove varTerm 55 def 21 ref appTerm appTerm 15 ref 22 ref absTerm 56 def appTerm appTerm refl 14 ref refl 57 def 23 ref 54 ref 55 ref 25 ref appTerm appTerm refl "_3145" 3 ref var 58 def 23 ref 15 ref 26 ref 58 remove varTerm 19 ref appTerm appTerm absTerm absTerm absTerm 59 def 55 remove 24 ref appTerm 60 def appTerm betaConv 24 ref refl 61 def appThm "n'" 1 ref var 15 ref 26 ref 60 remove 19 ref appTerm appTerm absTerm absTerm 24 ref appTerm betaConv trans appThm absThm appThm appThm absThm appThm nil "f" 0 ref 3 ref 33 remove cons opType var 59 remove nil cons cons "e" 3 remove var 56 ref nil cons cons nil cons cons nil cons cons "A" 4 remove cons nil cons 37 ref cons "f" 0 ref 39 ref 0 ref 1 ref 48 ref cons opType 62 def nil cons 63 def cons opType 64 def var 65 def "Data.Bool.?!" const 66 def 0 ref 0 ref 62 ref 8 ref cons opType 67 def 8 ref cons opType 68 def constTerm "fn" 62 remove var 69 def 11 ref 16 ref 0 ref 39 ref 40 ref nil cons cons opType constTerm 70 def 69 remove varTerm 71 def 21 ref appTerm appTerm "e" 39 ref var 72 def varTerm 73 def appTerm appTerm 14 ref 23 ref 70 ref 71 ref 25 ref appTerm appTerm 65 remove varTerm 74 def 71 remove 24 ref appTerm appTerm 24 ref appTerm appTerm absTerm appTerm appTerm absTerm 75 def appTerm 76 def absTerm 77 def 74 ref appTerm 78 def betaConv 72 remove 12 ref 0 ref 0 ref 64 ref 8 ref cons opType 79 def 8 ref cons opType constTerm 77 ref appTerm 80 def absTerm 81 def 73 ref appTerm 82 def betaConv nil 12 ref 41 ref constTerm 83 def 81 ref appTerm 84 def axiom nil "p" 7 ref var 85 def 84 remove nil cons cons "q" 7 ref var 86 def 82 remove nil cons cons nil cons cons nil cons cons 16 ref 10 ref constTerm 87 def "Data.Bool.==>" const 10 ref constTerm 88 def 85 ref varTerm 89 def appTerm 86 ref varTerm 90 def appTerm 91 def appTerm refl 85 ref 86 ref 87 ref 11 ref 89 ref appTerm 92 def 90 ref appTerm 93 def appTerm 94 def 89 ref appTerm absTerm 95 def absTerm 96 def 89 ref appTerm betaConv 90 ref refl 97 def appThm 95 remove 90 ref appTerm betaConv trans appThm nil 16 ref 0 ref 10 ref 0 ref 10 ref 8 ref cons opType 98 def nil cons cons opType constTerm 99 def 88 ref appTerm 96 remove appTerm axiom 89 ref refl 100 def appThm 97 ref appThm eqMp 101 def sym 102 def 94 remove refl 86 ref 16 ref 0 ref 98 ref 0 ref 98 remove 8 ref cons opType nil cons cons opType constTerm 103 def "f" 10 remove var 104 def 104 ref varTerm 105 def 89 ref appTerm 90 ref appTerm absTerm 106 def appTerm 104 ref 105 ref "Data.Bool.T" const 7 ref constTerm 107 def appTerm 107 ref appTerm absTerm 108 def appTerm absTerm 109 def 90 ref appTerm betaConv appThm 16 ref 0 ref 9 ref 0 ref 9 ref 8 ref cons opType 110 def nil cons cons opType constTerm 111 def 92 remove appTerm refl 85 ref 109 remove absTerm 112 def 89 ref appTerm betaConv appThm nil 99 remove 11 ref appTerm 112 ref appTerm axiom 113 def 100 remove appThm eqMp 97 ref appThm eqMp 114 def sym 104 ref 105 ref refl nil "t" 7 ref var 115 def 89 ref nil cons 116 def cons nil cons nil cons cons 87 ref 115 ref varTerm 117 def appTerm 107 ref appTerm assume sym nil 107 ref axiom 118 def eqMp 117 remove assume 118 ref deductAntisym deductAntisym 119 def subst 89 ref assume 120 def eqMp appThm nil 115 ref 90 ref nil cons 121 def cons nil cons nil cons cons 119 ref subst 90 ref assume eqMp appThm absThm eqMp 122 def nil "P" 7 ref var 123 def 116 remove cons "Q" 7 ref var 124 def 121 remove cons nil cons cons nil cons cons 87 ref refl 125 def 104 ref 105 remove 123 ref varTerm 126 def appTerm 127 def 124 ref varTerm 128 def appTerm absTerm 129 def 85 ref 86 ref 89 ref absTerm absTerm 130 def appTerm betaConv 130 ref 126 ref appTerm betaConv 128 ref refl 131 def appThm 86 ref 126 ref absTerm 128 ref appTerm betaConv trans trans appThm 108 ref 130 ref appTerm betaConv 130 ref 107 ref appTerm betaConv 107 ref refl 132 def appThm 86 ref 107 ref absTerm 107 ref appTerm betaConv trans trans appThm 87 ref 11 ref 126 ref appTerm 133 def 128 ref appTerm 134 def appTerm refl 86 ref 103 remove 104 remove 127 remove 90 ref appTerm absTerm appTerm 108 ref appTerm absTerm 128 ref appTerm betaConv appThm 111 remove 133 remove appTerm refl 112 remove 126 ref appTerm betaConv appThm 113 remove 126 ref refl appThm eqMp 131 ref appThm eqMp 134 remove assume eqMp 135 def 130 remove refl appThm eqMp sym 118 ref eqMp 136 def subst 137 def deductAntisym eqMp 101 remove 91 ref assume eqMp sym 120 ref eqMp 125 ref 106 remove 85 ref 86 ref 90 ref absTerm 138 def absTerm 139 def appTerm betaConv 139 ref 89 ref appTerm betaConv 97 remove appThm 138 ref 90 ref appTerm betaConv trans trans appThm 108 remove 139 ref appTerm betaConv 139 ref 107 ref appTerm betaConv 132 remove appThm 138 ref 107 ref appTerm betaConv trans trans 140 def appThm 114 remove 93 remove assume eqMp 139 ref refl 141 def appThm eqMp sym 118 ref eqMp 142 def proveHyp deductAntisym 143 def subst proveHyp "A" 48 remove cons nil cons 144 def "P" 40 ref var 145 def 81 remove nil cons cons "x" 39 ref var 146 def 73 remove nil cons cons nil cons cons nil cons cons nil 85 ref 83 ref 145 ref varTerm 147 def appTerm 148 def nil cons 149 def cons 86 ref 147 ref 146 ref varTerm 150 def appTerm 151 def nil cons 152 def cons nil cons cons nil cons cons 153 def 102 ref subst 153 remove 142 remove 122 remove deductAntisym 154 def subst 87 ref 151 ref appTerm refl 146 ref 107 remove absTerm 155 def 150 ref appTerm betaConv appThm 46 ref 16 remove 0 remove 40 remove 41 ref nil cons cons opType constTerm 47 ref appTerm 155 remove appTerm absTerm 156 def 147 ref appTerm betaConv 157 def nil 42 ref 83 ref appTerm 156 remove appTerm axiom 147 ref refl 158 def appThm 159 def 148 ref assume eqMp eqMp 150 ref refl appThm eqMp sym 118 ref eqMp eqMp nil 123 ref 149 remove cons 124 ref 152 ref cons nil cons cons nil cons cons 136 ref subst deductAntisym eqMp 160 def subst eqMp eqMp nil 85 ref 80 remove nil cons cons 86 ref 78 remove nil cons cons nil cons cons nil cons cons 143 ref subst proveHyp "A" 64 ref nil cons cons nil cons "P" 79 remove var 77 remove nil cons cons "x" 64 remove var 74 remove nil cons cons nil cons cons nil cons cons 160 ref subst eqMp eqMp nil 85 ref 76 remove nil cons cons 86 ref 43 remove 68 remove constTerm 75 ref appTerm nil cons cons nil cons cons nil cons cons 143 ref subst proveHyp "A" 63 remove cons nil cons "P" 67 remove var 75 remove nil cons cons nil cons nil cons cons nil 85 ref 66 remove 41 remove constTerm 161 def 147 ref appTerm 162 def nil cons 163 def cons 164 def 86 ref 44 ref 147 ref appTerm 165 def nil cons 166 def cons nil cons cons nil cons cons 167 def 102 ref subst 167 remove 154 ref subst nil 164 remove 86 ref 11 ref 165 ref appTerm 83 ref 146 ref 83 ref "y" 39 remove var 168 def 88 ref 11 ref 151 ref appTerm 147 ref 168 ref varTerm 169 def appTerm appTerm appTerm 70 remove 150 ref appTerm 169 ref appTerm 170 def appTerm absTerm appTerm absTerm appTerm 171 def appTerm 172 def nil cons cons nil cons cons nil cons cons 173 def 143 ref subst 87 ref 162 ref appTerm 174 def refl 46 ref 11 ref 44 remove 47 ref appTerm appTerm 83 ref 146 ref 83 ref 168 remove 88 ref 11 ref 47 ref 150 ref appTerm 175 def appTerm 47 remove 169 remove appTerm appTerm appTerm 170 remove appTerm absTerm appTerm absTerm appTerm appTerm absTerm 176 def 147 ref appTerm betaConv appThm nil 42 remove 161 remove appTerm 176 remove appTerm axiom 158 ref appThm eqMp nil 85 ref 174 remove 172 ref appTerm nil cons cons 86 ref 88 ref 162 remove appTerm 172 remove appTerm nil cons cons nil cons cons nil cons cons 143 ref subst proveHyp 173 remove nil 85 ref 87 ref 89 remove appTerm 90 ref appTerm 177 def nil cons 178 def cons 86 ref 91 remove nil cons 179 def cons nil cons cons nil cons cons 180 def 102 ref subst 180 remove 154 ref subst 102 ref 154 ref 177 remove assume 120 remove eqMp eqMp 137 remove deductAntisym eqMp eqMp nil 123 ref 178 remove cons 124 ref 179 remove cons nil cons cons nil cons cons 136 ref subst deductAntisym eqMp 181 def subst eqMp eqMp nil 123 ref 166 ref cons 182 def 124 ref 171 remove nil cons cons nil cons cons nil cons cons 136 ref subst proveHyp eqMp nil 123 ref 163 remove cons 124 ref 166 ref cons nil cons cons nil cons cons 136 ref subst deductAntisym eqMp subst eqMp subst subst eqMp nil 85 ref 52 ref "_3144" 5 ref var 183 def 11 ref 54 ref 183 ref varTerm 184 def 21 ref appTerm 185 def appTerm 56 ref appTerm 186 def appTerm 14 ref 23 ref 54 remove 184 ref 25 ref appTerm 187 def appTerm 15 ref 26 ref 184 ref 24 ref appTerm 19 ref appTerm appTerm 188 def absTerm 189 def appTerm absTerm 190 def appTerm 191 def appTerm 192 def absTerm 193 def appTerm 194 def nil cons cons 86 ref 52 ref 183 ref 11 ref 14 ref 15 ref 17 ref 185 remove 19 ref appTerm appTerm 195 def 22 ref appTerm 196 def absTerm 197 def appTerm 198 def appTerm 14 ref 15 ref 14 ref 23 ref 17 ref 187 remove 19 ref appTerm appTerm 199 def 188 remove appTerm 200 def absTerm 201 def appTerm 202 def absTerm 203 def appTerm 204 def appTerm 205 def absTerm 206 def appTerm 207 def nil cons 208 def cons nil cons 209 def cons nil cons cons 143 ref subst nil "P" 29 remove var 210 def 183 ref 88 ref 193 ref 184 ref appTerm 211 def appTerm 207 ref appTerm 212 def absTerm nil cons cons nil cons nil cons cons 38 remove 87 ref 148 remove appTerm refl 157 remove appThm 159 remove eqMp sym 213 def subst 214 def subst 183 ref nil 115 ref 212 remove nil cons cons nil cons nil cons cons 119 ref subst nil 85 ref 211 ref nil cons 215 def cons 209 ref cons nil cons cons 216 def 102 ref subst 216 remove 154 ref subst 211 ref betaConv 211 remove assume eqMp nil 85 ref 192 remove nil cons 217 def cons 209 remove cons nil cons cons 218 def 143 ref subst proveHyp 218 ref 102 ref subst 218 remove 154 ref subst 206 ref 184 ref appTerm 219 def betaConv 220 def sym nil 123 ref 186 ref nil cons cons 124 ref 191 remove nil cons 221 def cons nil cons cons nil cons cons 222 def 136 ref subst nil "P" 13 remove var 223 def 197 remove nil cons cons nil cons nil cons cons "A" 2 remove cons nil cons 224 def 37 ref cons 213 ref subst 225 def subst 15 ref nil 115 ref 196 remove nil cons cons nil cons nil cons cons 119 ref subst 195 remove refl 56 remove 19 ref appTerm betaConv appThm 186 remove assume 19 ref refl 226 def appThm eqMp eqMp absThm eqMp proveHyp nil 85 ref 198 remove nil cons cons 86 ref 204 remove nil cons cons nil cons cons nil cons cons 154 ref subst proveHyp 222 remove 125 remove 129 remove 139 ref appTerm betaConv 139 remove 126 remove appTerm betaConv 131 remove appThm 138 remove 128 ref appTerm betaConv trans trans appThm 140 remove appThm 135 remove 141 remove appThm eqMp sym 118 remove eqMp 227 def subst nil 223 ref 203 remove nil cons cons nil cons nil cons cons 225 ref subst 15 ref nil 115 ref 202 remove nil cons cons nil cons nil cons cons 119 ref subst nil 223 ref 201 remove nil cons cons nil cons nil cons cons 225 remove subst 23 ref nil 115 ref 200 remove nil cons cons nil cons nil cons cons 119 ref subst 199 remove refl 189 remove 19 ref appTerm betaConv appThm 190 ref 24 ref appTerm 228 def betaConv nil 85 ref 221 remove cons 86 ref 228 remove nil cons cons nil cons cons nil cons cons 143 ref subst 224 remove 223 remove 190 remove nil cons cons "x" 1 ref var 24 ref nil cons cons nil cons cons nil cons cons 160 ref subst eqMp eqMp 226 ref appThm eqMp eqMp absThm eqMp eqMp absThm eqMp proveHyp eqMp eqMp 36 ref 210 ref 206 ref nil cons cons 229 def "x" 5 ref var 230 def 184 ref nil cons cons nil cons cons nil cons cons 87 remove 165 ref appTerm 231 def refl 46 remove 12 ref 110 remove constTerm 232 def 86 ref 88 ref 83 ref 146 ref 88 ref 175 remove appTerm 90 ref appTerm absTerm appTerm appTerm 90 ref appTerm absTerm appTerm absTerm 233 def 147 remove appTerm betaConv appThm nil 45 remove 233 remove appTerm axiom 158 remove appThm eqMp 234 def sym nil "P" 9 remove var 235 def 124 ref 88 ref 83 ref 146 ref 88 ref 151 remove appTerm 236 def 128 ref appTerm absTerm 237 def appTerm 238 def appTerm 128 ref appTerm 239 def absTerm nil cons cons nil cons nil cons cons "A" 8 remove cons nil cons 240 def 37 remove cons 213 remove subst subst 124 ref nil 115 ref 239 remove nil cons cons nil cons nil cons cons 119 ref subst nil 85 ref 238 remove nil cons 241 def cons 242 def 86 ref 128 ref nil cons 243 def cons nil cons 244 def cons nil cons cons 245 def 102 ref subst 245 ref 154 ref subst nil 85 ref 152 remove cons 244 ref cons nil cons cons 143 ref subst 237 ref 150 ref appTerm 246 def betaConv nil 242 ref 86 ref 246 remove nil cons cons nil cons cons nil cons cons 143 ref subst 144 remove 145 remove 237 remove nil cons cons 146 ref 150 remove nil cons cons nil cons cons nil cons cons 160 ref subst eqMp eqMp eqMp eqMp nil 123 ref 241 remove cons 247 def 124 ref 243 ref cons nil cons 248 def cons nil cons cons 136 ref subst deductAntisym eqMp eqMp absThm eqMp eqMp 249 def subst proveHyp eqMp nil 123 ref 217 remove cons 124 ref 208 ref cons nil cons 250 def cons nil cons cons 136 ref subst deductAntisym eqMp eqMp eqMp nil 123 ref 215 remove cons 250 ref cons nil cons cons 136 ref subst deductAntisym eqMp eqMp absThm eqMp nil 85 ref 12 remove 51 remove constTerm 251 def 230 ref 88 ref 193 ref 230 ref varTerm 252 def appTerm appTerm 207 ref appTerm absTerm appTerm nil cons cons 86 ref 88 ref 194 remove appTerm 207 ref appTerm nil cons cons nil cons cons nil cons cons 143 ref subst proveHyp 36 ref 210 ref 193 remove nil cons cons 250 remove cons nil cons cons nil 242 remove 86 ref 88 ref 165 remove appTerm 253 def 128 ref appTerm nil cons 254 def cons nil cons cons nil cons cons 255 def 102 ref subst 255 remove 154 ref subst nil 85 ref 166 remove cons 256 def 244 remove cons nil cons cons 257 def 102 ref subst 257 remove 154 ref subst 245 remove 143 ref subst 86 ref 88 ref 83 remove 146 remove 236 remove 90 ref appTerm absTerm appTerm appTerm 90 remove appTerm absTerm 258 def 128 remove appTerm 259 def betaConv nil 256 remove 86 ref 232 remove 258 ref appTerm 260 def nil cons 261 def cons nil cons cons nil cons cons 262 def 143 ref subst 234 remove nil 85 ref 231 remove 260 ref appTerm nil cons cons 86 ref 253 remove 260 remove appTerm nil cons cons nil cons cons nil cons cons 143 ref subst proveHyp 262 remove 181 remove subst eqMp eqMp nil 85 ref 261 remove cons 86 ref 259 remove nil cons cons nil cons cons nil cons cons 143 ref subst proveHyp 240 remove 235 remove 258 remove nil cons cons "x" 7 remove var 243 remove cons nil cons cons nil cons cons 160 remove subst eqMp eqMp eqMp eqMp nil 182 remove 248 remove cons nil cons cons 136 ref subst deductAntisym eqMp eqMp nil 247 remove 124 ref 254 remove cons nil cons cons nil cons cons 136 ref subst deductAntisym eqMp 263 def subst eqMp eqMp proveHyp nil 85 ref 208 remove cons 86 ref 52 remove 27 ref appTerm 264 def nil cons 265 def cons nil cons 266 def cons nil cons cons 143 ref subst nil 210 ref 183 ref 88 ref 219 ref appTerm 264 ref appTerm 267 def absTerm nil cons cons nil cons nil cons cons 214 remove subst 183 remove nil 115 remove 267 remove nil cons cons nil cons nil cons cons 119 remove subst nil 85 ref 219 ref nil cons 268 def cons 266 ref cons nil cons cons 269 def 102 ref subst 269 remove 154 ref subst 220 remove 219 remove assume eqMp nil 85 ref 205 ref nil cons 270 def cons 266 ref cons nil cons cons 271 def 143 ref subst proveHyp 271 ref 102 ref subst 271 remove 154 ref subst "_3142" 1 ref var 272 def "_3143" 1 remove var 273 def 184 remove 273 ref varTerm appTerm 274 def 272 remove varTerm appTerm absTerm absTerm 275 def refl nil 85 ref 30 remove 275 ref appTerm 275 ref appTerm nil cons cons 266 ref cons nil cons cons 143 ref subst proveHyp nil 6 remove 275 ref nil cons cons nil cons nil cons cons nil 85 ref 31 remove 275 ref appTerm 276 def nil cons 277 def cons 266 remove cons nil cons cons 278 def 102 remove subst 278 remove 154 remove subst 35 remove sym 11 remove refl 57 ref 15 ref 17 ref refl 279 def 276 remove assume 226 remove appThm 275 remove 19 ref appTerm betaConv trans 280 def nil 23 ref 21 ref nil cons cons nil cons nil cons cons 61 ref subst appThm 273 remove 274 remove 19 ref appTerm absTerm 281 def 21 ref appTerm betaConv trans appThm 22 ref refl appThm absThm appThm appThm 57 ref 15 ref 57 remove 23 ref 279 remove 280 ref 25 ref refl appThm 281 ref 25 ref appTerm betaConv trans appThm 26 ref refl 280 remove 61 remove appThm 281 remove 24 ref appTerm betaConv trans appThm appThm absThm appThm absThm appThm appThm sym 205 remove assume eqMp eqMp 36 ref 210 remove 27 remove nil cons cons 230 ref 18 remove nil cons cons nil cons cons nil cons cons 249 remove subst proveHyp eqMp nil 123 ref 277 remove cons 124 ref 265 remove cons nil cons 282 def cons nil cons cons 136 ref subst deductAntisym eqMp subst eqMp eqMp nil 123 ref 270 remove cons 282 ref cons nil cons cons 136 ref subst deductAntisym eqMp eqMp eqMp nil 123 ref 268 remove cons 282 ref cons nil cons cons 136 ref subst deductAntisym eqMp eqMp absThm eqMp nil 85 remove 251 remove 230 remove 88 ref 206 remove 252 remove appTerm appTerm 264 ref appTerm absTerm appTerm nil cons cons 86 remove 88 remove 207 remove appTerm 264 remove appTerm nil cons cons nil cons cons nil cons cons 143 remove subst proveHyp 36 remove 229 remove 282 remove cons nil cons cons 263 remove subst eqMp eqMp proveHyp eqMp eqMp defineConstList 283 def pop 284 def pop 283 ref nil 123 remove 14 ref 15 ref 17 ref 284 remove hdTl pop 5 remove constTerm 19 remove appTerm 285 def 21 remove appTerm appTerm 22 remove appTerm absTerm appTerm 286 def nil cons cons 124 remove 14 ref 15 remove 14 remove 23 remove 17 remove 285 ref 25 remove appTerm appTerm 26 remove 285 remove 24 remove appTerm appTerm appTerm absTerm appTerm absTerm appTerm 287 def nil cons cons nil cons cons nil cons cons 288 def 227 remove subst proveHyp nil 287 remove thm 283 remove 288 remove 136 remove subst proveHyp nil 286 remove thm