def facts_4

bendtorch-core@0.1.0.0 · src/tensor/axis_algebra.bend:2256

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/tensor/axis_spec.bend as Axis

2256def facts_4(+axes: List<&2, Nat>, accepted: {True{} == Axis.valid(4n, axes) : Bool}) -> Facts<4n, axes>:
2257  match axes:
2258    case Nil{}:
2259      Empty.absurd(Facts<4n, Nil{}>, Shape.clash(accepted))
2260    case +a0 <> Nil{}:
2261      Empty.absurd(Facts<4n, a0 <> Nil{}>, Shape.clash(accepted))
2262    case +a0 <> +a1 <> Nil{}:
2263      Empty.absurd(Facts<4n, a0 <> a1 <> Nil{}>, Shape.clash(accepted))
2264    case +a0 <> +a1 <> +a2 <> Nil{}:
2265      Empty.absurd(Facts<4n, a0 <> a1 <> a2 <> Nil{}>, Shape.clash(accepted))
2266    case 0n <> 0n <> 0n <> 0n <> Nil{}:
2267      Empty.absurd(Facts<4n, [0n, 0n, 0n, 0n]>, Shape.clash(accepted))
2268    case 0n <> 0n <> 0n <> 1n <> Nil{}:
2269      Empty.absurd(Facts<4n, [0n, 0n, 0n, 1n]>, Shape.clash(accepted))
2270    case 0n <> 0n <> 0n <> 2n <> Nil{}:
2271      Empty.absurd(Facts<4n, [0n, 0n, 0n, 2n]>, Shape.clash(accepted))
2272    case 0n <> 0n <> 0n <> 3n <> Nil{}:
2273      Empty.absurd(Facts<4n, [0n, 0n, 0n, 3n]>, Shape.clash(accepted))
2274    case 0n <> 0n <> 0n <> (4n+p) <> Nil{}:
2275      Empty.absurd(Facts<4n, 0n <> 0n <> 0n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(0n <> 0n <> 0n <> (4n+p) <> Nil{}, 4n), Axis.unique(0n <> 0n <> 0n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 0n <> 0n <> 0n <> (4n+p) <> Nil{}), accepted)))))
2276    case 0n <> 0n <> 1n <> 0n <> Nil{}:
2277      Empty.absurd(Facts<4n, [0n, 0n, 1n, 0n]>, Shape.clash(accepted))
2278    case 0n <> 0n <> 1n <> 1n <> Nil{}:
2279      Empty.absurd(Facts<4n, [0n, 0n, 1n, 1n]>, Shape.clash(accepted))
2280    case 0n <> 0n <> 1n <> 2n <> Nil{}:
2281      Empty.absurd(Facts<4n, [0n, 0n, 1n, 2n]>, Shape.clash(accepted))
2282    case 0n <> 0n <> 1n <> 3n <> Nil{}:
2283      Empty.absurd(Facts<4n, [0n, 0n, 1n, 3n]>, Shape.clash(accepted))
2284    case 0n <> 0n <> 1n <> (4n+p) <> Nil{}:
2285      Empty.absurd(Facts<4n, 0n <> 0n <> 1n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(0n <> 0n <> 1n <> (4n+p) <> Nil{}, 4n), Axis.unique(0n <> 0n <> 1n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 0n <> 0n <> 1n <> (4n+p) <> Nil{}), accepted)))))
2286    case 0n <> 0n <> 2n <> 0n <> Nil{}:
2287      Empty.absurd(Facts<4n, [0n, 0n, 2n, 0n]>, Shape.clash(accepted))
2288    case 0n <> 0n <> 2n <> 1n <> Nil{}:
2289      Empty.absurd(Facts<4n, [0n, 0n, 2n, 1n]>, Shape.clash(accepted))
2290    case 0n <> 0n <> 2n <> 2n <> Nil{}:
2291      Empty.absurd(Facts<4n, [0n, 0n, 2n, 2n]>, Shape.clash(accepted))
2292    case 0n <> 0n <> 2n <> 3n <> Nil{}:
2293      Empty.absurd(Facts<4n, [0n, 0n, 2n, 3n]>, Shape.clash(accepted))
2294    case 0n <> 0n <> 2n <> (4n+p) <> Nil{}:
2295      Empty.absurd(Facts<4n, 0n <> 0n <> 2n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(0n <> 0n <> 2n <> (4n+p) <> Nil{}, 4n), Axis.unique(0n <> 0n <> 2n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 0n <> 0n <> 2n <> (4n+p) <> Nil{}), accepted)))))
2296    case 0n <> 0n <> 3n <> 0n <> Nil{}:
2297      Empty.absurd(Facts<4n, [0n, 0n, 3n, 0n]>, Shape.clash(accepted))
2298    case 0n <> 0n <> 3n <> 1n <> Nil{}:
2299      Empty.absurd(Facts<4n, [0n, 0n, 3n, 1n]>, Shape.clash(accepted))
2300    case 0n <> 0n <> 3n <> 2n <> Nil{}:
2301      Empty.absurd(Facts<4n, [0n, 0n, 3n, 2n]>, Shape.clash(accepted))
2302    case 0n <> 0n <> 3n <> 3n <> Nil{}:
2303      Empty.absurd(Facts<4n, [0n, 0n, 3n, 3n]>, Shape.clash(accepted))
2304    case 0n <> 0n <> 3n <> (4n+p) <> Nil{}:
2305      Empty.absurd(Facts<4n, 0n <> 0n <> 3n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(0n <> 0n <> 3n <> (4n+p) <> Nil{}, 4n), Axis.unique(0n <> 0n <> 3n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 0n <> 0n <> 3n <> (4n+p) <> Nil{}), accepted)))))
2306    case 0n <> 0n <> (4n+p) <> a0 <> Nil{}:
2307      Empty.absurd(Facts<4n, 0n <> 0n <> (4n+p) <> a0 <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(a0 <> Nil{}, 4n), Arith.and_left(Axis.bounded(0n <> 0n <> (4n+p) <> a0 <> Nil{}, 4n), Axis.unique(0n <> 0n <> (4n+p) <> a0 <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 0n <> 0n <> (4n+p) <> a0 <> Nil{}), accepted)))))
2308    case 0n <> 1n <> 0n <> 0n <> Nil{}:
2309      Empty.absurd(Facts<4n, [0n, 1n, 0n, 0n]>, Shape.clash(accepted))
2310    case 0n <> 1n <> 0n <> 1n <> Nil{}:
2311      Empty.absurd(Facts<4n, [0n, 1n, 0n, 1n]>, Shape.clash(accepted))
2312    case 0n <> 1n <> 0n <> 2n <> Nil{}:
2313      Empty.absurd(Facts<4n, [0n, 1n, 0n, 2n]>, Shape.clash(accepted))
2314    case 0n <> 1n <> 0n <> 3n <> Nil{}:
2315      Empty.absurd(Facts<4n, [0n, 1n, 0n, 3n]>, Shape.clash(accepted))
2316    case 0n <> 1n <> 0n <> (4n+p) <> Nil{}:
2317      Empty.absurd(Facts<4n, 0n <> 1n <> 0n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(0n <> 1n <> 0n <> (4n+p) <> Nil{}, 4n), Axis.unique(0n <> 1n <> 0n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 0n <> 1n <> 0n <> (4n+p) <> Nil{}), accepted)))))
2318    case 0n <> 1n <> 1n <> 0n <> Nil{}:
2319      Empty.absurd(Facts<4n, [0n, 1n, 1n, 0n]>, Shape.clash(accepted))
2320    case 0n <> 1n <> 1n <> 1n <> Nil{}:
2321      Empty.absurd(Facts<4n, [0n, 1n, 1n, 1n]>, Shape.clash(accepted))
2322    case 0n <> 1n <> 1n <> 2n <> Nil{}:
2323      Empty.absurd(Facts<4n, [0n, 1n, 1n, 2n]>, Shape.clash(accepted))
2324    case 0n <> 1n <> 1n <> 3n <> Nil{}:
2325      Empty.absurd(Facts<4n, [0n, 1n, 1n, 3n]>, Shape.clash(accepted))
2326    case 0n <> 1n <> 1n <> (4n+p) <> Nil{}:
2327      Empty.absurd(Facts<4n, 0n <> 1n <> 1n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(0n <> 1n <> 1n <> (4n+p) <> Nil{}, 4n), Axis.unique(0n <> 1n <> 1n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 0n <> 1n <> 1n <> (4n+p) <> Nil{}), accepted)))))
2328    case 0n <> 1n <> 2n <> 0n <> Nil{}:
2329      Empty.absurd(Facts<4n, [0n, 1n, 2n, 0n]>, Shape.clash(accepted))
2330    case 0n <> 1n <> 2n <> 1n <> Nil{}:
2331      Empty.absurd(Facts<4n, [0n, 1n, 2n, 1n]>, Shape.clash(accepted))
2332    case 0n <> 1n <> 2n <> 2n <> Nil{}:
2333      Empty.absurd(Facts<4n, [0n, 1n, 2n, 2n]>, Shape.clash(accepted))
2334    case 0n <> 1n <> 2n <> 3n <> Nil{}:
2335      Certified{{==}, {==}, {==}, A => items => length => lists_0123(A, items, length),
2336        dims => length => product_0123(dims, length), dims => coords => dl => cl => fit_0123(dims, coords, dl, cl)}
2337    case 0n <> 1n <> 2n <> (4n+p) <> Nil{}:
2338      Empty.absurd(Facts<4n, 0n <> 1n <> 2n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(0n <> 1n <> 2n <> (4n+p) <> Nil{}, 4n), Axis.unique(0n <> 1n <> 2n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 0n <> 1n <> 2n <> (4n+p) <> Nil{}), accepted)))))
2339    case 0n <> 1n <> 3n <> 0n <> Nil{}:
2340      Empty.absurd(Facts<4n, [0n, 1n, 3n, 0n]>, Shape.clash(accepted))
2341    case 0n <> 1n <> 3n <> 1n <> Nil{}:
2342      Empty.absurd(Facts<4n, [0n, 1n, 3n, 1n]>, Shape.clash(accepted))
2343    case 0n <> 1n <> 3n <> 2n <> Nil{}:
2344      Certified{{==}, {==}, {==}, A => items => length => lists_0132(A, items, length),
2345        dims => length => product_0132(dims, length), dims => coords => dl => cl => fit_0132(dims, coords, dl, cl)}
2346    case 0n <> 1n <> 3n <> 3n <> Nil{}:
2347      Empty.absurd(Facts<4n, [0n, 1n, 3n, 3n]>, Shape.clash(accepted))
2348    case 0n <> 1n <> 3n <> (4n+p) <> Nil{}:
2349      Empty.absurd(Facts<4n, 0n <> 1n <> 3n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(0n <> 1n <> 3n <> (4n+p) <> Nil{}, 4n), Axis.unique(0n <> 1n <> 3n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 0n <> 1n <> 3n <> (4n+p) <> Nil{}), accepted)))))
2350    case 0n <> 1n <> (4n+p) <> a0 <> Nil{}:
2351      Empty.absurd(Facts<4n, 0n <> 1n <> (4n+p) <> a0 <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(a0 <> Nil{}, 4n), Arith.and_left(Axis.bounded(0n <> 1n <> (4n+p) <> a0 <> Nil{}, 4n), Axis.unique(0n <> 1n <> (4n+p) <> a0 <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 0n <> 1n <> (4n+p) <> a0 <> Nil{}), accepted)))))
2352    case 0n <> 2n <> 0n <> 0n <> Nil{}:
2353      Empty.absurd(Facts<4n, [0n, 2n, 0n, 0n]>, Shape.clash(accepted))
2354    case 0n <> 2n <> 0n <> 1n <> Nil{}:
2355      Empty.absurd(Facts<4n, [0n, 2n, 0n, 1n]>, Shape.clash(accepted))
2356    case 0n <> 2n <> 0n <> 2n <> Nil{}:
2357      Empty.absurd(Facts<4n, [0n, 2n, 0n, 2n]>, Shape.clash(accepted))
2358    case 0n <> 2n <> 0n <> 3n <> Nil{}:
2359      Empty.absurd(Facts<4n, [0n, 2n, 0n, 3n]>, Shape.clash(accepted))
2360    case 0n <> 2n <> 0n <> (4n+p) <> Nil{}:
2361      Empty.absurd(Facts<4n, 0n <> 2n <> 0n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(0n <> 2n <> 0n <> (4n+p) <> Nil{}, 4n), Axis.unique(0n <> 2n <> 0n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 0n <> 2n <> 0n <> (4n+p) <> Nil{}), accepted)))))
2362    case 0n <> 2n <> 1n <> 0n <> Nil{}:
2363      Empty.absurd(Facts<4n, [0n, 2n, 1n, 0n]>, Shape.clash(accepted))
2364    case 0n <> 2n <> 1n <> 1n <> Nil{}:
2365      Empty.absurd(Facts<4n, [0n, 2n, 1n, 1n]>, Shape.clash(accepted))
2366    case 0n <> 2n <> 1n <> 2n <> Nil{}:
2367      Empty.absurd(Facts<4n, [0n, 2n, 1n, 2n]>, Shape.clash(accepted))
2368    case 0n <> 2n <> 1n <> 3n <> Nil{}:
2369      Certified{{==}, {==}, {==}, A => items => length => lists_0213(A, items, length),
2370        dims => length => product_0213(dims, length), dims => coords => dl => cl => fit_0213(dims, coords, dl, cl)}
2371    case 0n <> 2n <> 1n <> (4n+p) <> Nil{}:
2372      Empty.absurd(Facts<4n, 0n <> 2n <> 1n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(0n <> 2n <> 1n <> (4n+p) <> Nil{}, 4n), Axis.unique(0n <> 2n <> 1n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 0n <> 2n <> 1n <> (4n+p) <> Nil{}), accepted)))))
2373    case 0n <> 2n <> 2n <> 0n <> Nil{}:
2374      Empty.absurd(Facts<4n, [0n, 2n, 2n, 0n]>, Shape.clash(accepted))
2375    case 0n <> 2n <> 2n <> 1n <> Nil{}:
2376      Empty.absurd(Facts<4n, [0n, 2n, 2n, 1n]>, Shape.clash(accepted))
2377    case 0n <> 2n <> 2n <> 2n <> Nil{}:
2378      Empty.absurd(Facts<4n, [0n, 2n, 2n, 2n]>, Shape.clash(accepted))
2379    case 0n <> 2n <> 2n <> 3n <> Nil{}:
2380      Empty.absurd(Facts<4n, [0n, 2n, 2n, 3n]>, Shape.clash(accepted))
2381    case 0n <> 2n <> 2n <> (4n+p) <> Nil{}:
2382      Empty.absurd(Facts<4n, 0n <> 2n <> 2n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(0n <> 2n <> 2n <> (4n+p) <> Nil{}, 4n), Axis.unique(0n <> 2n <> 2n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 0n <> 2n <> 2n <> (4n+p) <> Nil{}), accepted)))))
2383    case 0n <> 2n <> 3n <> 0n <> Nil{}:
2384      Empty.absurd(Facts<4n, [0n, 2n, 3n, 0n]>, Shape.clash(accepted))
2385    case 0n <> 2n <> 3n <> 1n <> Nil{}:
2386      Certified{{==}, {==}, {==}, A => items => length => lists_0231(A, items, length),
2387        dims => length => product_0231(dims, length), dims => coords => dl => cl => fit_0231(dims, coords, dl, cl)}
2388    case 0n <> 2n <> 3n <> 2n <> Nil{}:
2389      Empty.absurd(Facts<4n, [0n, 2n, 3n, 2n]>, Shape.clash(accepted))
2390    case 0n <> 2n <> 3n <> 3n <> Nil{}:
2391      Empty.absurd(Facts<4n, [0n, 2n, 3n, 3n]>, Shape.clash(accepted))
2392    case 0n <> 2n <> 3n <> (4n+p) <> Nil{}:
2393      Empty.absurd(Facts<4n, 0n <> 2n <> 3n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(0n <> 2n <> 3n <> (4n+p) <> Nil{}, 4n), Axis.unique(0n <> 2n <> 3n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 0n <> 2n <> 3n <> (4n+p) <> Nil{}), accepted)))))
2394    case 0n <> 2n <> (4n+p) <> a0 <> Nil{}:
2395      Empty.absurd(Facts<4n, 0n <> 2n <> (4n+p) <> a0 <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(a0 <> Nil{}, 4n), Arith.and_left(Axis.bounded(0n <> 2n <> (4n+p) <> a0 <> Nil{}, 4n), Axis.unique(0n <> 2n <> (4n+p) <> a0 <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 0n <> 2n <> (4n+p) <> a0 <> Nil{}), accepted)))))
2396    case 0n <> 3n <> 0n <> 0n <> Nil{}:
2397      Empty.absurd(Facts<4n, [0n, 3n, 0n, 0n]>, Shape.clash(accepted))
2398    case 0n <> 3n <> 0n <> 1n <> Nil{}:
2399      Empty.absurd(Facts<4n, [0n, 3n, 0n, 1n]>, Shape.clash(accepted))
2400    case 0n <> 3n <> 0n <> 2n <> Nil{}:
2401      Empty.absurd(Facts<4n, [0n, 3n, 0n, 2n]>, Shape.clash(accepted))
2402    case 0n <> 3n <> 0n <> 3n <> Nil{}:
2403      Empty.absurd(Facts<4n, [0n, 3n, 0n, 3n]>, Shape.clash(accepted))
2404    case 0n <> 3n <> 0n <> (4n+p) <> Nil{}:
2405      Empty.absurd(Facts<4n, 0n <> 3n <> 0n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(0n <> 3n <> 0n <> (4n+p) <> Nil{}, 4n), Axis.unique(0n <> 3n <> 0n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 0n <> 3n <> 0n <> (4n+p) <> Nil{}), accepted)))))
2406    case 0n <> 3n <> 1n <> 0n <> Nil{}:
2407      Empty.absurd(Facts<4n, [0n, 3n, 1n, 0n]>, Shape.clash(accepted))
2408    case 0n <> 3n <> 1n <> 1n <> Nil{}:
2409      Empty.absurd(Facts<4n, [0n, 3n, 1n, 1n]>, Shape.clash(accepted))
2410    case 0n <> 3n <> 1n <> 2n <> Nil{}:
2411      Certified{{==}, {==}, {==}, A => items => length => lists_0312(A, items, length),
2412        dims => length => product_0312(dims, length), dims => coords => dl => cl => fit_0312(dims, coords, dl, cl)}
2413    case 0n <> 3n <> 1n <> 3n <> Nil{}:
2414      Empty.absurd(Facts<4n, [0n, 3n, 1n, 3n]>, Shape.clash(accepted))
2415    case 0n <> 3n <> 1n <> (4n+p) <> Nil{}:
2416      Empty.absurd(Facts<4n, 0n <> 3n <> 1n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(0n <> 3n <> 1n <> (4n+p) <> Nil{}, 4n), Axis.unique(0n <> 3n <> 1n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 0n <> 3n <> 1n <> (4n+p) <> Nil{}), accepted)))))
2417    case 0n <> 3n <> 2n <> 0n <> Nil{}:
2418      Empty.absurd(Facts<4n, [0n, 3n, 2n, 0n]>, Shape.clash(accepted))
2419    case 0n <> 3n <> 2n <> 1n <> Nil{}:
2420      Certified{{==}, {==}, {==}, A => items => length => lists_0321(A, items, length),
2421        dims => length => product_0321(dims, length), dims => coords => dl => cl => fit_0321(dims, coords, dl, cl)}
2422    case 0n <> 3n <> 2n <> 2n <> Nil{}:
2423      Empty.absurd(Facts<4n, [0n, 3n, 2n, 2n]>, Shape.clash(accepted))
2424    case 0n <> 3n <> 2n <> 3n <> Nil{}:
2425      Empty.absurd(Facts<4n, [0n, 3n, 2n, 3n]>, Shape.clash(accepted))
2426    case 0n <> 3n <> 2n <> (4n+p) <> Nil{}:
2427      Empty.absurd(Facts<4n, 0n <> 3n <> 2n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(0n <> 3n <> 2n <> (4n+p) <> Nil{}, 4n), Axis.unique(0n <> 3n <> 2n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 0n <> 3n <> 2n <> (4n+p) <> Nil{}), accepted)))))
2428    case 0n <> 3n <> 3n <> 0n <> Nil{}:
2429      Empty.absurd(Facts<4n, [0n, 3n, 3n, 0n]>, Shape.clash(accepted))
2430    case 0n <> 3n <> 3n <> 1n <> Nil{}:
2431      Empty.absurd(Facts<4n, [0n, 3n, 3n, 1n]>, Shape.clash(accepted))
2432    case 0n <> 3n <> 3n <> 2n <> Nil{}:
2433      Empty.absurd(Facts<4n, [0n, 3n, 3n, 2n]>, Shape.clash(accepted))
2434    case 0n <> 3n <> 3n <> 3n <> Nil{}:
2435      Empty.absurd(Facts<4n, [0n, 3n, 3n, 3n]>, Shape.clash(accepted))
2436    case 0n <> 3n <> 3n <> (4n+p) <> Nil{}:
2437      Empty.absurd(Facts<4n, 0n <> 3n <> 3n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(0n <> 3n <> 3n <> (4n+p) <> Nil{}, 4n), Axis.unique(0n <> 3n <> 3n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 0n <> 3n <> 3n <> (4n+p) <> Nil{}), accepted)))))
2438    case 0n <> 3n <> (4n+p) <> a0 <> Nil{}:
2439      Empty.absurd(Facts<4n, 0n <> 3n <> (4n+p) <> a0 <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(a0 <> Nil{}, 4n), Arith.and_left(Axis.bounded(0n <> 3n <> (4n+p) <> a0 <> Nil{}, 4n), Axis.unique(0n <> 3n <> (4n+p) <> a0 <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 0n <> 3n <> (4n+p) <> a0 <> Nil{}), accepted)))))
2440    case 0n <> (4n+p) <> a0 <> a1 <> Nil{}:
2441      Empty.absurd(Facts<4n, 0n <> (4n+p) <> a0 <> a1 <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(a0 <> a1 <> Nil{}, 4n), Arith.and_left(Axis.bounded(0n <> (4n+p) <> a0 <> a1 <> Nil{}, 4n), Axis.unique(0n <> (4n+p) <> a0 <> a1 <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 0n <> (4n+p) <> a0 <> a1 <> Nil{}), accepted)))))
2442    case 1n <> 0n <> 0n <> 0n <> Nil{}:
2443      Empty.absurd(Facts<4n, [1n, 0n, 0n, 0n]>, Shape.clash(accepted))
2444    case 1n <> 0n <> 0n <> 1n <> Nil{}:
2445      Empty.absurd(Facts<4n, [1n, 0n, 0n, 1n]>, Shape.clash(accepted))
2446    case 1n <> 0n <> 0n <> 2n <> Nil{}:
2447      Empty.absurd(Facts<4n, [1n, 0n, 0n, 2n]>, Shape.clash(accepted))
2448    case 1n <> 0n <> 0n <> 3n <> Nil{}:
2449      Empty.absurd(Facts<4n, [1n, 0n, 0n, 3n]>, Shape.clash(accepted))
2450    case 1n <> 0n <> 0n <> (4n+p) <> Nil{}:
2451      Empty.absurd(Facts<4n, 1n <> 0n <> 0n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(1n <> 0n <> 0n <> (4n+p) <> Nil{}, 4n), Axis.unique(1n <> 0n <> 0n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 1n <> 0n <> 0n <> (4n+p) <> Nil{}), accepted)))))
2452    case 1n <> 0n <> 1n <> 0n <> Nil{}:
2453      Empty.absurd(Facts<4n, [1n, 0n, 1n, 0n]>, Shape.clash(accepted))
2454    case 1n <> 0n <> 1n <> 1n <> Nil{}:
2455      Empty.absurd(Facts<4n, [1n, 0n, 1n, 1n]>, Shape.clash(accepted))
2456    case 1n <> 0n <> 1n <> 2n <> Nil{}:
2457      Empty.absurd(Facts<4n, [1n, 0n, 1n, 2n]>, Shape.clash(accepted))
2458    case 1n <> 0n <> 1n <> 3n <> Nil{}:
2459      Empty.absurd(Facts<4n, [1n, 0n, 1n, 3n]>, Shape.clash(accepted))
2460    case 1n <> 0n <> 1n <> (4n+p) <> Nil{}:
2461      Empty.absurd(Facts<4n, 1n <> 0n <> 1n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(1n <> 0n <> 1n <> (4n+p) <> Nil{}, 4n), Axis.unique(1n <> 0n <> 1n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 1n <> 0n <> 1n <> (4n+p) <> Nil{}), accepted)))))
2462    case 1n <> 0n <> 2n <> 0n <> Nil{}:
2463      Empty.absurd(Facts<4n, [1n, 0n, 2n, 0n]>, Shape.clash(accepted))
2464    case 1n <> 0n <> 2n <> 1n <> Nil{}:
2465      Empty.absurd(Facts<4n, [1n, 0n, 2n, 1n]>, Shape.clash(accepted))
2466    case 1n <> 0n <> 2n <> 2n <> Nil{}:
2467      Empty.absurd(Facts<4n, [1n, 0n, 2n, 2n]>, Shape.clash(accepted))
2468    case 1n <> 0n <> 2n <> 3n <> Nil{}:
2469      Certified{{==}, {==}, {==}, A => items => length => lists_1023(A, items, length),
2470        dims => length => product_1023(dims, length), dims => coords => dl => cl => fit_1023(dims, coords, dl, cl)}
2471    case 1n <> 0n <> 2n <> (4n+p) <> Nil{}:
2472      Empty.absurd(Facts<4n, 1n <> 0n <> 2n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(1n <> 0n <> 2n <> (4n+p) <> Nil{}, 4n), Axis.unique(1n <> 0n <> 2n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 1n <> 0n <> 2n <> (4n+p) <> Nil{}), accepted)))))
2473    case 1n <> 0n <> 3n <> 0n <> Nil{}:
2474      Empty.absurd(Facts<4n, [1n, 0n, 3n, 0n]>, Shape.clash(accepted))
2475    case 1n <> 0n <> 3n <> 1n <> Nil{}:
2476      Empty.absurd(Facts<4n, [1n, 0n, 3n, 1n]>, Shape.clash(accepted))
2477    case 1n <> 0n <> 3n <> 2n <> Nil{}:
2478      Certified{{==}, {==}, {==}, A => items => length => lists_1032(A, items, length),
2479        dims => length => product_1032(dims, length), dims => coords => dl => cl => fit_1032(dims, coords, dl, cl)}
2480    case 1n <> 0n <> 3n <> 3n <> Nil{}:
2481      Empty.absurd(Facts<4n, [1n, 0n, 3n, 3n]>, Shape.clash(accepted))
2482    case 1n <> 0n <> 3n <> (4n+p) <> Nil{}:
2483      Empty.absurd(Facts<4n, 1n <> 0n <> 3n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(1n <> 0n <> 3n <> (4n+p) <> Nil{}, 4n), Axis.unique(1n <> 0n <> 3n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 1n <> 0n <> 3n <> (4n+p) <> Nil{}), accepted)))))
2484    case 1n <> 0n <> (4n+p) <> a0 <> Nil{}:
2485      Empty.absurd(Facts<4n, 1n <> 0n <> (4n+p) <> a0 <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(a0 <> Nil{}, 4n), Arith.and_left(Axis.bounded(1n <> 0n <> (4n+p) <> a0 <> Nil{}, 4n), Axis.unique(1n <> 0n <> (4n+p) <> a0 <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 1n <> 0n <> (4n+p) <> a0 <> Nil{}), accepted)))))
2486    case 1n <> 1n <> 0n <> 0n <> Nil{}:
2487      Empty.absurd(Facts<4n, [1n, 1n, 0n, 0n]>, Shape.clash(accepted))
2488    case 1n <> 1n <> 0n <> 1n <> Nil{}:
2489      Empty.absurd(Facts<4n, [1n, 1n, 0n, 1n]>, Shape.clash(accepted))
2490    case 1n <> 1n <> 0n <> 2n <> Nil{}:
2491      Empty.absurd(Facts<4n, [1n, 1n, 0n, 2n]>, Shape.clash(accepted))
2492    case 1n <> 1n <> 0n <> 3n <> Nil{}:
2493      Empty.absurd(Facts<4n, [1n, 1n, 0n, 3n]>, Shape.clash(accepted))
2494    case 1n <> 1n <> 0n <> (4n+p) <> Nil{}:
2495      Empty.absurd(Facts<4n, 1n <> 1n <> 0n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(1n <> 1n <> 0n <> (4n+p) <> Nil{}, 4n), Axis.unique(1n <> 1n <> 0n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 1n <> 1n <> 0n <> (4n+p) <> Nil{}), accepted)))))
2496    case 1n <> 1n <> 1n <> 0n <> Nil{}:
2497      Empty.absurd(Facts<4n, [1n, 1n, 1n, 0n]>, Shape.clash(accepted))
2498    case 1n <> 1n <> 1n <> 1n <> Nil{}:
2499      Empty.absurd(Facts<4n, [1n, 1n, 1n, 1n]>, Shape.clash(accepted))
2500    case 1n <> 1n <> 1n <> 2n <> Nil{}:
2501      Empty.absurd(Facts<4n, [1n, 1n, 1n, 2n]>, Shape.clash(accepted))
2502    case 1n <> 1n <> 1n <> 3n <> Nil{}:
2503      Empty.absurd(Facts<4n, [1n, 1n, 1n, 3n]>, Shape.clash(accepted))
2504    case 1n <> 1n <> 1n <> (4n+p) <> Nil{}:
2505      Empty.absurd(Facts<4n, 1n <> 1n <> 1n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(1n <> 1n <> 1n <> (4n+p) <> Nil{}, 4n), Axis.unique(1n <> 1n <> 1n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 1n <> 1n <> 1n <> (4n+p) <> Nil{}), accepted)))))
2506    case 1n <> 1n <> 2n <> 0n <> Nil{}:
2507      Empty.absurd(Facts<4n, [1n, 1n, 2n, 0n]>, Shape.clash(accepted))
2508    case 1n <> 1n <> 2n <> 1n <> Nil{}:
2509      Empty.absurd(Facts<4n, [1n, 1n, 2n, 1n]>, Shape.clash(accepted))
2510    case 1n <> 1n <> 2n <> 2n <> Nil{}:
2511      Empty.absurd(Facts<4n, [1n, 1n, 2n, 2n]>, Shape.clash(accepted))
2512    case 1n <> 1n <> 2n <> 3n <> Nil{}:
2513      Empty.absurd(Facts<4n, [1n, 1n, 2n, 3n]>, Shape.clash(accepted))
2514    case 1n <> 1n <> 2n <> (4n+p) <> Nil{}:
2515      Empty.absurd(Facts<4n, 1n <> 1n <> 2n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(1n <> 1n <> 2n <> (4n+p) <> Nil{}, 4n), Axis.unique(1n <> 1n <> 2n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 1n <> 1n <> 2n <> (4n+p) <> Nil{}), accepted)))))
2516    case 1n <> 1n <> 3n <> 0n <> Nil{}:
2517      Empty.absurd(Facts<4n, [1n, 1n, 3n, 0n]>, Shape.clash(accepted))
2518    case 1n <> 1n <> 3n <> 1n <> Nil{}:
2519      Empty.absurd(Facts<4n, [1n, 1n, 3n, 1n]>, Shape.clash(accepted))
2520    case 1n <> 1n <> 3n <> 2n <> Nil{}:
2521      Empty.absurd(Facts<4n, [1n, 1n, 3n, 2n]>, Shape.clash(accepted))
2522    case 1n <> 1n <> 3n <> 3n <> Nil{}:
2523      Empty.absurd(Facts<4n, [1n, 1n, 3n, 3n]>, Shape.clash(accepted))
2524    case 1n <> 1n <> 3n <> (4n+p) <> Nil{}:
2525      Empty.absurd(Facts<4n, 1n <> 1n <> 3n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(1n <> 1n <> 3n <> (4n+p) <> Nil{}, 4n), Axis.unique(1n <> 1n <> 3n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 1n <> 1n <> 3n <> (4n+p) <> Nil{}), accepted)))))
2526    case 1n <> 1n <> (4n+p) <> a0 <> Nil{}:
2527      Empty.absurd(Facts<4n, 1n <> 1n <> (4n+p) <> a0 <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(a0 <> Nil{}, 4n), Arith.and_left(Axis.bounded(1n <> 1n <> (4n+p) <> a0 <> Nil{}, 4n), Axis.unique(1n <> 1n <> (4n+p) <> a0 <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 1n <> 1n <> (4n+p) <> a0 <> Nil{}), accepted)))))
2528    case 1n <> 2n <> 0n <> 0n <> Nil{}:
2529      Empty.absurd(Facts<4n, [1n, 2n, 0n, 0n]>, Shape.clash(accepted))
2530    case 1n <> 2n <> 0n <> 1n <> Nil{}:
2531      Empty.absurd(Facts<4n, [1n, 2n, 0n, 1n]>, Shape.clash(accepted))
2532    case 1n <> 2n <> 0n <> 2n <> Nil{}:
2533      Empty.absurd(Facts<4n, [1n, 2n, 0n, 2n]>, Shape.clash(accepted))
2534    case 1n <> 2n <> 0n <> 3n <> Nil{}:
2535      Certified{{==}, {==}, {==}, A => items => length => lists_1203(A, items, length),
2536        dims => length => product_1203(dims, length), dims => coords => dl => cl => fit_1203(dims, coords, dl, cl)}
2537    case 1n <> 2n <> 0n <> (4n+p) <> Nil{}:
2538      Empty.absurd(Facts<4n, 1n <> 2n <> 0n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(1n <> 2n <> 0n <> (4n+p) <> Nil{}, 4n), Axis.unique(1n <> 2n <> 0n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 1n <> 2n <> 0n <> (4n+p) <> Nil{}), accepted)))))
2539    case 1n <> 2n <> 1n <> 0n <> Nil{}:
2540      Empty.absurd(Facts<4n, [1n, 2n, 1n, 0n]>, Shape.clash(accepted))
2541    case 1n <> 2n <> 1n <> 1n <> Nil{}:
2542      Empty.absurd(Facts<4n, [1n, 2n, 1n, 1n]>, Shape.clash(accepted))
2543    case 1n <> 2n <> 1n <> 2n <> Nil{}:
2544      Empty.absurd(Facts<4n, [1n, 2n, 1n, 2n]>, Shape.clash(accepted))
2545    case 1n <> 2n <> 1n <> 3n <> Nil{}:
2546      Empty.absurd(Facts<4n, [1n, 2n, 1n, 3n]>, Shape.clash(accepted))
2547    case 1n <> 2n <> 1n <> (4n+p) <> Nil{}:
2548      Empty.absurd(Facts<4n, 1n <> 2n <> 1n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(1n <> 2n <> 1n <> (4n+p) <> Nil{}, 4n), Axis.unique(1n <> 2n <> 1n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 1n <> 2n <> 1n <> (4n+p) <> Nil{}), accepted)))))
2549    case 1n <> 2n <> 2n <> 0n <> Nil{}:
2550      Empty.absurd(Facts<4n, [1n, 2n, 2n, 0n]>, Shape.clash(accepted))
2551    case 1n <> 2n <> 2n <> 1n <> Nil{}:
2552      Empty.absurd(Facts<4n, [1n, 2n, 2n, 1n]>, Shape.clash(accepted))
2553    case 1n <> 2n <> 2n <> 2n <> Nil{}:
2554      Empty.absurd(Facts<4n, [1n, 2n, 2n, 2n]>, Shape.clash(accepted))
2555    case 1n <> 2n <> 2n <> 3n <> Nil{}:
2556      Empty.absurd(Facts<4n, [1n, 2n, 2n, 3n]>, Shape.clash(accepted))
2557    case 1n <> 2n <> 2n <> (4n+p) <> Nil{}:
2558      Empty.absurd(Facts<4n, 1n <> 2n <> 2n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(1n <> 2n <> 2n <> (4n+p) <> Nil{}, 4n), Axis.unique(1n <> 2n <> 2n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 1n <> 2n <> 2n <> (4n+p) <> Nil{}), accepted)))))
2559    case 1n <> 2n <> 3n <> 0n <> Nil{}:
2560      Certified{{==}, {==}, {==}, A => items => length => lists_1230(A, items, length),
2561        dims => length => product_1230(dims, length), dims => coords => dl => cl => fit_1230(dims, coords, dl, cl)}
2562    case 1n <> 2n <> 3n <> 1n <> Nil{}:
2563      Empty.absurd(Facts<4n, [1n, 2n, 3n, 1n]>, Shape.clash(accepted))
2564    case 1n <> 2n <> 3n <> 2n <> Nil{}:
2565      Empty.absurd(Facts<4n, [1n, 2n, 3n, 2n]>, Shape.clash(accepted))
2566    case 1n <> 2n <> 3n <> 3n <> Nil{}:
2567      Empty.absurd(Facts<4n, [1n, 2n, 3n, 3n]>, Shape.clash(accepted))
2568    case 1n <> 2n <> 3n <> (4n+p) <> Nil{}:
2569      Empty.absurd(Facts<4n, 1n <> 2n <> 3n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(1n <> 2n <> 3n <> (4n+p) <> Nil{}, 4n), Axis.unique(1n <> 2n <> 3n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 1n <> 2n <> 3n <> (4n+p) <> Nil{}), accepted)))))
2570    case 1n <> 2n <> (4n+p) <> a0 <> Nil{}:
2571      Empty.absurd(Facts<4n, 1n <> 2n <> (4n+p) <> a0 <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(a0 <> Nil{}, 4n), Arith.and_left(Axis.bounded(1n <> 2n <> (4n+p) <> a0 <> Nil{}, 4n), Axis.unique(1n <> 2n <> (4n+p) <> a0 <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 1n <> 2n <> (4n+p) <> a0 <> Nil{}), accepted)))))
2572    case 1n <> 3n <> 0n <> 0n <> Nil{}:
2573      Empty.absurd(Facts<4n, [1n, 3n, 0n, 0n]>, Shape.clash(accepted))
2574    case 1n <> 3n <> 0n <> 1n <> Nil{}:
2575      Empty.absurd(Facts<4n, [1n, 3n, 0n, 1n]>, Shape.clash(accepted))
2576    case 1n <> 3n <> 0n <> 2n <> Nil{}:
2577      Certified{{==}, {==}, {==}, A => items => length => lists_1302(A, items, length),
2578        dims => length => product_1302(dims, length), dims => coords => dl => cl => fit_1302(dims, coords, dl, cl)}
2579    case 1n <> 3n <> 0n <> 3n <> Nil{}:
2580      Empty.absurd(Facts<4n, [1n, 3n, 0n, 3n]>, Shape.clash(accepted))
2581    case 1n <> 3n <> 0n <> (4n+p) <> Nil{}:
2582      Empty.absurd(Facts<4n, 1n <> 3n <> 0n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(1n <> 3n <> 0n <> (4n+p) <> Nil{}, 4n), Axis.unique(1n <> 3n <> 0n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 1n <> 3n <> 0n <> (4n+p) <> Nil{}), accepted)))))
2583    case 1n <> 3n <> 1n <> 0n <> Nil{}:
2584      Empty.absurd(Facts<4n, [1n, 3n, 1n, 0n]>, Shape.clash(accepted))
2585    case 1n <> 3n <> 1n <> 1n <> Nil{}:
2586      Empty.absurd(Facts<4n, [1n, 3n, 1n, 1n]>, Shape.clash(accepted))
2587    case 1n <> 3n <> 1n <> 2n <> Nil{}:
2588      Empty.absurd(Facts<4n, [1n, 3n, 1n, 2n]>, Shape.clash(accepted))
2589    case 1n <> 3n <> 1n <> 3n <> Nil{}:
2590      Empty.absurd(Facts<4n, [1n, 3n, 1n, 3n]>, Shape.clash(accepted))
2591    case 1n <> 3n <> 1n <> (4n+p) <> Nil{}:
2592      Empty.absurd(Facts<4n, 1n <> 3n <> 1n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(1n <> 3n <> 1n <> (4n+p) <> Nil{}, 4n), Axis.unique(1n <> 3n <> 1n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 1n <> 3n <> 1n <> (4n+p) <> Nil{}), accepted)))))
2593    case 1n <> 3n <> 2n <> 0n <> Nil{}:
2594      Certified{{==}, {==}, {==}, A => items => length => lists_1320(A, items, length),
2595        dims => length => product_1320(dims, length), dims => coords => dl => cl => fit_1320(dims, coords, dl, cl)}
2596    case 1n <> 3n <> 2n <> 1n <> Nil{}:
2597      Empty.absurd(Facts<4n, [1n, 3n, 2n, 1n]>, Shape.clash(accepted))
2598    case 1n <> 3n <> 2n <> 2n <> Nil{}:
2599      Empty.absurd(Facts<4n, [1n, 3n, 2n, 2n]>, Shape.clash(accepted))
2600    case 1n <> 3n <> 2n <> 3n <> Nil{}:
2601      Empty.absurd(Facts<4n, [1n, 3n, 2n, 3n]>, Shape.clash(accepted))
2602    case 1n <> 3n <> 2n <> (4n+p) <> Nil{}:
2603      Empty.absurd(Facts<4n, 1n <> 3n <> 2n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(1n <> 3n <> 2n <> (4n+p) <> Nil{}, 4n), Axis.unique(1n <> 3n <> 2n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 1n <> 3n <> 2n <> (4n+p) <> Nil{}), accepted)))))
2604    case 1n <> 3n <> 3n <> 0n <> Nil{}:
2605      Empty.absurd(Facts<4n, [1n, 3n, 3n, 0n]>, Shape.clash(accepted))
2606    case 1n <> 3n <> 3n <> 1n <> Nil{}:
2607      Empty.absurd(Facts<4n, [1n, 3n, 3n, 1n]>, Shape.clash(accepted))
2608    case 1n <> 3n <> 3n <> 2n <> Nil{}:
2609      Empty.absurd(Facts<4n, [1n, 3n, 3n, 2n]>, Shape.clash(accepted))
2610    case 1n <> 3n <> 3n <> 3n <> Nil{}:
2611      Empty.absurd(Facts<4n, [1n, 3n, 3n, 3n]>, Shape.clash(accepted))
2612    case 1n <> 3n <> 3n <> (4n+p) <> Nil{}:
2613      Empty.absurd(Facts<4n, 1n <> 3n <> 3n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(1n <> 3n <> 3n <> (4n+p) <> Nil{}, 4n), Axis.unique(1n <> 3n <> 3n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 1n <> 3n <> 3n <> (4n+p) <> Nil{}), accepted)))))
2614    case 1n <> 3n <> (4n+p) <> a0 <> Nil{}:
2615      Empty.absurd(Facts<4n, 1n <> 3n <> (4n+p) <> a0 <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(a0 <> Nil{}, 4n), Arith.and_left(Axis.bounded(1n <> 3n <> (4n+p) <> a0 <> Nil{}, 4n), Axis.unique(1n <> 3n <> (4n+p) <> a0 <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 1n <> 3n <> (4n+p) <> a0 <> Nil{}), accepted)))))
2616    case 1n <> (4n+p) <> a0 <> a1 <> Nil{}:
2617      Empty.absurd(Facts<4n, 1n <> (4n+p) <> a0 <> a1 <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(a0 <> a1 <> Nil{}, 4n), Arith.and_left(Axis.bounded(1n <> (4n+p) <> a0 <> a1 <> Nil{}, 4n), Axis.unique(1n <> (4n+p) <> a0 <> a1 <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 1n <> (4n+p) <> a0 <> a1 <> Nil{}), accepted)))))
2618    case 2n <> 0n <> 0n <> 0n <> Nil{}:
2619      Empty.absurd(Facts<4n, [2n, 0n, 0n, 0n]>, Shape.clash(accepted))
2620    case 2n <> 0n <> 0n <> 1n <> Nil{}:
2621      Empty.absurd(Facts<4n, [2n, 0n, 0n, 1n]>, Shape.clash(accepted))
2622    case 2n <> 0n <> 0n <> 2n <> Nil{}:
2623      Empty.absurd(Facts<4n, [2n, 0n, 0n, 2n]>, Shape.clash(accepted))
2624    case 2n <> 0n <> 0n <> 3n <> Nil{}:
2625      Empty.absurd(Facts<4n, [2n, 0n, 0n, 3n]>, Shape.clash(accepted))
2626    case 2n <> 0n <> 0n <> (4n+p) <> Nil{}:
2627      Empty.absurd(Facts<4n, 2n <> 0n <> 0n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(2n <> 0n <> 0n <> (4n+p) <> Nil{}, 4n), Axis.unique(2n <> 0n <> 0n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 2n <> 0n <> 0n <> (4n+p) <> Nil{}), accepted)))))
2628    case 2n <> 0n <> 1n <> 0n <> Nil{}:
2629      Empty.absurd(Facts<4n, [2n, 0n, 1n, 0n]>, Shape.clash(accepted))
2630    case 2n <> 0n <> 1n <> 1n <> Nil{}:
2631      Empty.absurd(Facts<4n, [2n, 0n, 1n, 1n]>, Shape.clash(accepted))
2632    case 2n <> 0n <> 1n <> 2n <> Nil{}:
2633      Empty.absurd(Facts<4n, [2n, 0n, 1n, 2n]>, Shape.clash(accepted))
2634    case 2n <> 0n <> 1n <> 3n <> Nil{}:
2635      Certified{{==}, {==}, {==}, A => items => length => lists_2013(A, items, length),
2636        dims => length => product_2013(dims, length), dims => coords => dl => cl => fit_2013(dims, coords, dl, cl)}
2637    case 2n <> 0n <> 1n <> (4n+p) <> Nil{}:
2638      Empty.absurd(Facts<4n, 2n <> 0n <> 1n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(2n <> 0n <> 1n <> (4n+p) <> Nil{}, 4n), Axis.unique(2n <> 0n <> 1n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 2n <> 0n <> 1n <> (4n+p) <> Nil{}), accepted)))))
2639    case 2n <> 0n <> 2n <> 0n <> Nil{}:
2640      Empty.absurd(Facts<4n, [2n, 0n, 2n, 0n]>, Shape.clash(accepted))
2641    case 2n <> 0n <> 2n <> 1n <> Nil{}:
2642      Empty.absurd(Facts<4n, [2n, 0n, 2n, 1n]>, Shape.clash(accepted))
2643    case 2n <> 0n <> 2n <> 2n <> Nil{}:
2644      Empty.absurd(Facts<4n, [2n, 0n, 2n, 2n]>, Shape.clash(accepted))
2645    case 2n <> 0n <> 2n <> 3n <> Nil{}:
2646      Empty.absurd(Facts<4n, [2n, 0n, 2n, 3n]>, Shape.clash(accepted))
2647    case 2n <> 0n <> 2n <> (4n+p) <> Nil{}:
2648      Empty.absurd(Facts<4n, 2n <> 0n <> 2n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(2n <> 0n <> 2n <> (4n+p) <> Nil{}, 4n), Axis.unique(2n <> 0n <> 2n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 2n <> 0n <> 2n <> (4n+p) <> Nil{}), accepted)))))
2649    case 2n <> 0n <> 3n <> 0n <> Nil{}:
2650      Empty.absurd(Facts<4n, [2n, 0n, 3n, 0n]>, Shape.clash(accepted))
2651    case 2n <> 0n <> 3n <> 1n <> Nil{}:
2652      Certified{{==}, {==}, {==}, A => items => length => lists_2031(A, items, length),
2653        dims => length => product_2031(dims, length), dims => coords => dl => cl => fit_2031(dims, coords, dl, cl)}
2654    case 2n <> 0n <> 3n <> 2n <> Nil{}:
2655      Empty.absurd(Facts<4n, [2n, 0n, 3n, 2n]>, Shape.clash(accepted))
2656    case 2n <> 0n <> 3n <> 3n <> Nil{}:
2657      Empty.absurd(Facts<4n, [2n, 0n, 3n, 3n]>, Shape.clash(accepted))
2658    case 2n <> 0n <> 3n <> (4n+p) <> Nil{}:
2659      Empty.absurd(Facts<4n, 2n <> 0n <> 3n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(2n <> 0n <> 3n <> (4n+p) <> Nil{}, 4n), Axis.unique(2n <> 0n <> 3n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 2n <> 0n <> 3n <> (4n+p) <> Nil{}), accepted)))))
2660    case 2n <> 0n <> (4n+p) <> a0 <> Nil{}:
2661      Empty.absurd(Facts<4n, 2n <> 0n <> (4n+p) <> a0 <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(a0 <> Nil{}, 4n), Arith.and_left(Axis.bounded(2n <> 0n <> (4n+p) <> a0 <> Nil{}, 4n), Axis.unique(2n <> 0n <> (4n+p) <> a0 <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 2n <> 0n <> (4n+p) <> a0 <> Nil{}), accepted)))))
2662    case 2n <> 1n <> 0n <> 0n <> Nil{}:
2663      Empty.absurd(Facts<4n, [2n, 1n, 0n, 0n]>, Shape.clash(accepted))
2664    case 2n <> 1n <> 0n <> 1n <> Nil{}:
2665      Empty.absurd(Facts<4n, [2n, 1n, 0n, 1n]>, Shape.clash(accepted))
2666    case 2n <> 1n <> 0n <> 2n <> Nil{}:
2667      Empty.absurd(Facts<4n, [2n, 1n, 0n, 2n]>, Shape.clash(accepted))
2668    case 2n <> 1n <> 0n <> 3n <> Nil{}:
2669      Certified{{==}, {==}, {==}, A => items => length => lists_2103(A, items, length),
2670        dims => length => product_2103(dims, length), dims => coords => dl => cl => fit_2103(dims, coords, dl, cl)}
2671    case 2n <> 1n <> 0n <> (4n+p) <> Nil{}:
2672      Empty.absurd(Facts<4n, 2n <> 1n <> 0n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(2n <> 1n <> 0n <> (4n+p) <> Nil{}, 4n), Axis.unique(2n <> 1n <> 0n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 2n <> 1n <> 0n <> (4n+p) <> Nil{}), accepted)))))
2673    case 2n <> 1n <> 1n <> 0n <> Nil{}:
2674      Empty.absurd(Facts<4n, [2n, 1n, 1n, 0n]>, Shape.clash(accepted))
2675    case 2n <> 1n <> 1n <> 1n <> Nil{}:
2676      Empty.absurd(Facts<4n, [2n, 1n, 1n, 1n]>, Shape.clash(accepted))
2677    case 2n <> 1n <> 1n <> 2n <> Nil{}:
2678      Empty.absurd(Facts<4n, [2n, 1n, 1n, 2n]>, Shape.clash(accepted))
2679    case 2n <> 1n <> 1n <> 3n <> Nil{}:
2680      Empty.absurd(Facts<4n, [2n, 1n, 1n, 3n]>, Shape.clash(accepted))
2681    case 2n <> 1n <> 1n <> (4n+p) <> Nil{}:
2682      Empty.absurd(Facts<4n, 2n <> 1n <> 1n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(2n <> 1n <> 1n <> (4n+p) <> Nil{}, 4n), Axis.unique(2n <> 1n <> 1n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 2n <> 1n <> 1n <> (4n+p) <> Nil{}), accepted)))))
2683    case 2n <> 1n <> 2n <> 0n <> Nil{}:
2684      Empty.absurd(Facts<4n, [2n, 1n, 2n, 0n]>, Shape.clash(accepted))
2685    case 2n <> 1n <> 2n <> 1n <> Nil{}:
2686      Empty.absurd(Facts<4n, [2n, 1n, 2n, 1n]>, Shape.clash(accepted))
2687    case 2n <> 1n <> 2n <> 2n <> Nil{}:
2688      Empty.absurd(Facts<4n, [2n, 1n, 2n, 2n]>, Shape.clash(accepted))
2689    case 2n <> 1n <> 2n <> 3n <> Nil{}:
2690      Empty.absurd(Facts<4n, [2n, 1n, 2n, 3n]>, Shape.clash(accepted))
2691    case 2n <> 1n <> 2n <> (4n+p) <> Nil{}:
2692      Empty.absurd(Facts<4n, 2n <> 1n <> 2n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(2n <> 1n <> 2n <> (4n+p) <> Nil{}, 4n), Axis.unique(2n <> 1n <> 2n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 2n <> 1n <> 2n <> (4n+p) <> Nil{}), accepted)))))
2693    case 2n <> 1n <> 3n <> 0n <> Nil{}:
2694      Certified{{==}, {==}, {==}, A => items => length => lists_2130(A, items, length),
2695        dims => length => product_2130(dims, length), dims => coords => dl => cl => fit_2130(dims, coords, dl, cl)}
2696    case 2n <> 1n <> 3n <> 1n <> Nil{}:
2697      Empty.absurd(Facts<4n, [2n, 1n, 3n, 1n]>, Shape.clash(accepted))
2698    case 2n <> 1n <> 3n <> 2n <> Nil{}:
2699      Empty.absurd(Facts<4n, [2n, 1n, 3n, 2n]>, Shape.clash(accepted))
2700    case 2n <> 1n <> 3n <> 3n <> Nil{}:
2701      Empty.absurd(Facts<4n, [2n, 1n, 3n, 3n]>, Shape.clash(accepted))
2702    case 2n <> 1n <> 3n <> (4n+p) <> Nil{}:
2703      Empty.absurd(Facts<4n, 2n <> 1n <> 3n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(2n <> 1n <> 3n <> (4n+p) <> Nil{}, 4n), Axis.unique(2n <> 1n <> 3n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 2n <> 1n <> 3n <> (4n+p) <> Nil{}), accepted)))))
2704    case 2n <> 1n <> (4n+p) <> a0 <> Nil{}:
2705      Empty.absurd(Facts<4n, 2n <> 1n <> (4n+p) <> a0 <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(a0 <> Nil{}, 4n), Arith.and_left(Axis.bounded(2n <> 1n <> (4n+p) <> a0 <> Nil{}, 4n), Axis.unique(2n <> 1n <> (4n+p) <> a0 <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 2n <> 1n <> (4n+p) <> a0 <> Nil{}), accepted)))))
2706    case 2n <> 2n <> 0n <> 0n <> Nil{}:
2707      Empty.absurd(Facts<4n, [2n, 2n, 0n, 0n]>, Shape.clash(accepted))
2708    case 2n <> 2n <> 0n <> 1n <> Nil{}:
2709      Empty.absurd(Facts<4n, [2n, 2n, 0n, 1n]>, Shape.clash(accepted))
2710    case 2n <> 2n <> 0n <> 2n <> Nil{}:
2711      Empty.absurd(Facts<4n, [2n, 2n, 0n, 2n]>, Shape.clash(accepted))
2712    case 2n <> 2n <> 0n <> 3n <> Nil{}:
2713      Empty.absurd(Facts<4n, [2n, 2n, 0n, 3n]>, Shape.clash(accepted))
2714    case 2n <> 2n <> 0n <> (4n+p) <> Nil{}:
2715      Empty.absurd(Facts<4n, 2n <> 2n <> 0n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(2n <> 2n <> 0n <> (4n+p) <> Nil{}, 4n), Axis.unique(2n <> 2n <> 0n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 2n <> 2n <> 0n <> (4n+p) <> Nil{}), accepted)))))
2716    case 2n <> 2n <> 1n <> 0n <> Nil{}:
2717      Empty.absurd(Facts<4n, [2n, 2n, 1n, 0n]>, Shape.clash(accepted))
2718    case 2n <> 2n <> 1n <> 1n <> Nil{}:
2719      Empty.absurd(Facts<4n, [2n, 2n, 1n, 1n]>, Shape.clash(accepted))
2720    case 2n <> 2n <> 1n <> 2n <> Nil{}:
2721      Empty.absurd(Facts<4n, [2n, 2n, 1n, 2n]>, Shape.clash(accepted))
2722    case 2n <> 2n <> 1n <> 3n <> Nil{}:
2723      Empty.absurd(Facts<4n, [2n, 2n, 1n, 3n]>, Shape.clash(accepted))
2724    case 2n <> 2n <> 1n <> (4n+p) <> Nil{}:
2725      Empty.absurd(Facts<4n, 2n <> 2n <> 1n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(2n <> 2n <> 1n <> (4n+p) <> Nil{}, 4n), Axis.unique(2n <> 2n <> 1n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 2n <> 2n <> 1n <> (4n+p) <> Nil{}), accepted)))))
2726    case 2n <> 2n <> 2n <> 0n <> Nil{}:
2727      Empty.absurd(Facts<4n, [2n, 2n, 2n, 0n]>, Shape.clash(accepted))
2728    case 2n <> 2n <> 2n <> 1n <> Nil{}:
2729      Empty.absurd(Facts<4n, [2n, 2n, 2n, 1n]>, Shape.clash(accepted))
2730    case 2n <> 2n <> 2n <> 2n <> Nil{}:
2731      Empty.absurd(Facts<4n, [2n, 2n, 2n, 2n]>, Shape.clash(accepted))
2732    case 2n <> 2n <> 2n <> 3n <> Nil{}:
2733      Empty.absurd(Facts<4n, [2n, 2n, 2n, 3n]>, Shape.clash(accepted))
2734    case 2n <> 2n <> 2n <> (4n+p) <> Nil{}:
2735      Empty.absurd(Facts<4n, 2n <> 2n <> 2n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(2n <> 2n <> 2n <> (4n+p) <> Nil{}, 4n), Axis.unique(2n <> 2n <> 2n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 2n <> 2n <> 2n <> (4n+p) <> Nil{}), accepted)))))
2736    case 2n <> 2n <> 3n <> 0n <> Nil{}:
2737      Empty.absurd(Facts<4n, [2n, 2n, 3n, 0n]>, Shape.clash(accepted))
2738    case 2n <> 2n <> 3n <> 1n <> Nil{}:
2739      Empty.absurd(Facts<4n, [2n, 2n, 3n, 1n]>, Shape.clash(accepted))
2740    case 2n <> 2n <> 3n <> 2n <> Nil{}:
2741      Empty.absurd(Facts<4n, [2n, 2n, 3n, 2n]>, Shape.clash(accepted))
2742    case 2n <> 2n <> 3n <> 3n <> Nil{}:
2743      Empty.absurd(Facts<4n, [2n, 2n, 3n, 3n]>, Shape.clash(accepted))
2744    case 2n <> 2n <> 3n <> (4n+p) <> Nil{}:
2745      Empty.absurd(Facts<4n, 2n <> 2n <> 3n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(2n <> 2n <> 3n <> (4n+p) <> Nil{}, 4n), Axis.unique(2n <> 2n <> 3n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 2n <> 2n <> 3n <> (4n+p) <> Nil{}), accepted)))))
2746    case 2n <> 2n <> (4n+p) <> a0 <> Nil{}:
2747      Empty.absurd(Facts<4n, 2n <> 2n <> (4n+p) <> a0 <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(a0 <> Nil{}, 4n), Arith.and_left(Axis.bounded(2n <> 2n <> (4n+p) <> a0 <> Nil{}, 4n), Axis.unique(2n <> 2n <> (4n+p) <> a0 <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 2n <> 2n <> (4n+p) <> a0 <> Nil{}), accepted)))))
2748    case 2n <> 3n <> 0n <> 0n <> Nil{}:
2749      Empty.absurd(Facts<4n, [2n, 3n, 0n, 0n]>, Shape.clash(accepted))
2750    case 2n <> 3n <> 0n <> 1n <> Nil{}:
2751      Certified{{==}, {==}, {==}, A => items => length => lists_2301(A, items, length),
2752        dims => length => product_2301(dims, length), dims => coords => dl => cl => fit_2301(dims, coords, dl, cl)}
2753    case 2n <> 3n <> 0n <> 2n <> Nil{}:
2754      Empty.absurd(Facts<4n, [2n, 3n, 0n, 2n]>, Shape.clash(accepted))
2755    case 2n <> 3n <> 0n <> 3n <> Nil{}:
2756      Empty.absurd(Facts<4n, [2n, 3n, 0n, 3n]>, Shape.clash(accepted))
2757    case 2n <> 3n <> 0n <> (4n+p) <> Nil{}:
2758      Empty.absurd(Facts<4n, 2n <> 3n <> 0n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(2n <> 3n <> 0n <> (4n+p) <> Nil{}, 4n), Axis.unique(2n <> 3n <> 0n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 2n <> 3n <> 0n <> (4n+p) <> Nil{}), accepted)))))
2759    case 2n <> 3n <> 1n <> 0n <> Nil{}:
2760      Certified{{==}, {==}, {==}, A => items => length => lists_2310(A, items, length),
2761        dims => length => product_2310(dims, length), dims => coords => dl => cl => fit_2310(dims, coords, dl, cl)}
2762    case 2n <> 3n <> 1n <> 1n <> Nil{}:
2763      Empty.absurd(Facts<4n, [2n, 3n, 1n, 1n]>, Shape.clash(accepted))
2764    case 2n <> 3n <> 1n <> 2n <> Nil{}:
2765      Empty.absurd(Facts<4n, [2n, 3n, 1n, 2n]>, Shape.clash(accepted))
2766    case 2n <> 3n <> 1n <> 3n <> Nil{}:
2767      Empty.absurd(Facts<4n, [2n, 3n, 1n, 3n]>, Shape.clash(accepted))
2768    case 2n <> 3n <> 1n <> (4n+p) <> Nil{}:
2769      Empty.absurd(Facts<4n, 2n <> 3n <> 1n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(2n <> 3n <> 1n <> (4n+p) <> Nil{}, 4n), Axis.unique(2n <> 3n <> 1n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 2n <> 3n <> 1n <> (4n+p) <> Nil{}), accepted)))))
2770    case 2n <> 3n <> 2n <> 0n <> Nil{}:
2771      Empty.absurd(Facts<4n, [2n, 3n, 2n, 0n]>, Shape.clash(accepted))
2772    case 2n <> 3n <> 2n <> 1n <> Nil{}:
2773      Empty.absurd(Facts<4n, [2n, 3n, 2n, 1n]>, Shape.clash(accepted))
2774    case 2n <> 3n <> 2n <> 2n <> Nil{}:
2775      Empty.absurd(Facts<4n, [2n, 3n, 2n, 2n]>, Shape.clash(accepted))
2776    case 2n <> 3n <> 2n <> 3n <> Nil{}:
2777      Empty.absurd(Facts<4n, [2n, 3n, 2n, 3n]>, Shape.clash(accepted))
2778    case 2n <> 3n <> 2n <> (4n+p) <> Nil{}:
2779      Empty.absurd(Facts<4n, 2n <> 3n <> 2n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(2n <> 3n <> 2n <> (4n+p) <> Nil{}, 4n), Axis.unique(2n <> 3n <> 2n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 2n <> 3n <> 2n <> (4n+p) <> Nil{}), accepted)))))
2780    case 2n <> 3n <> 3n <> 0n <> Nil{}:
2781      Empty.absurd(Facts<4n, [2n, 3n, 3n, 0n]>, Shape.clash(accepted))
2782    case 2n <> 3n <> 3n <> 1n <> Nil{}:
2783      Empty.absurd(Facts<4n, [2n, 3n, 3n, 1n]>, Shape.clash(accepted))
2784    case 2n <> 3n <> 3n <> 2n <> Nil{}:
2785      Empty.absurd(Facts<4n, [2n, 3n, 3n, 2n]>, Shape.clash(accepted))
2786    case 2n <> 3n <> 3n <> 3n <> Nil{}:
2787      Empty.absurd(Facts<4n, [2n, 3n, 3n, 3n]>, Shape.clash(accepted))
2788    case 2n <> 3n <> 3n <> (4n+p) <> Nil{}:
2789      Empty.absurd(Facts<4n, 2n <> 3n <> 3n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(2n <> 3n <> 3n <> (4n+p) <> Nil{}, 4n), Axis.unique(2n <> 3n <> 3n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 2n <> 3n <> 3n <> (4n+p) <> Nil{}), accepted)))))
2790    case 2n <> 3n <> (4n+p) <> a0 <> Nil{}:
2791      Empty.absurd(Facts<4n, 2n <> 3n <> (4n+p) <> a0 <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(a0 <> Nil{}, 4n), Arith.and_left(Axis.bounded(2n <> 3n <> (4n+p) <> a0 <> Nil{}, 4n), Axis.unique(2n <> 3n <> (4n+p) <> a0 <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 2n <> 3n <> (4n+p) <> a0 <> Nil{}), accepted)))))
2792    case 2n <> (4n+p) <> a0 <> a1 <> Nil{}:
2793      Empty.absurd(Facts<4n, 2n <> (4n+p) <> a0 <> a1 <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(a0 <> a1 <> Nil{}, 4n), Arith.and_left(Axis.bounded(2n <> (4n+p) <> a0 <> a1 <> Nil{}, 4n), Axis.unique(2n <> (4n+p) <> a0 <> a1 <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 2n <> (4n+p) <> a0 <> a1 <> Nil{}), accepted)))))
2794    case 3n <> 0n <> 0n <> 0n <> Nil{}:
2795      Empty.absurd(Facts<4n, [3n, 0n, 0n, 0n]>, Shape.clash(accepted))
2796    case 3n <> 0n <> 0n <> 1n <> Nil{}:
2797      Empty.absurd(Facts<4n, [3n, 0n, 0n, 1n]>, Shape.clash(accepted))
2798    case 3n <> 0n <> 0n <> 2n <> Nil{}:
2799      Empty.absurd(Facts<4n, [3n, 0n, 0n, 2n]>, Shape.clash(accepted))
2800    case 3n <> 0n <> 0n <> 3n <> Nil{}:
2801      Empty.absurd(Facts<4n, [3n, 0n, 0n, 3n]>, Shape.clash(accepted))
2802    case 3n <> 0n <> 0n <> (4n+p) <> Nil{}:
2803      Empty.absurd(Facts<4n, 3n <> 0n <> 0n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(3n <> 0n <> 0n <> (4n+p) <> Nil{}, 4n), Axis.unique(3n <> 0n <> 0n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 3n <> 0n <> 0n <> (4n+p) <> Nil{}), accepted)))))
2804    case 3n <> 0n <> 1n <> 0n <> Nil{}:
2805      Empty.absurd(Facts<4n, [3n, 0n, 1n, 0n]>, Shape.clash(accepted))
2806    case 3n <> 0n <> 1n <> 1n <> Nil{}:
2807      Empty.absurd(Facts<4n, [3n, 0n, 1n, 1n]>, Shape.clash(accepted))
2808    case 3n <> 0n <> 1n <> 2n <> Nil{}:
2809      Certified{{==}, {==}, {==}, A => items => length => lists_3012(A, items, length),
2810        dims => length => product_3012(dims, length), dims => coords => dl => cl => fit_3012(dims, coords, dl, cl)}
2811    case 3n <> 0n <> 1n <> 3n <> Nil{}:
2812      Empty.absurd(Facts<4n, [3n, 0n, 1n, 3n]>, Shape.clash(accepted))
2813    case 3n <> 0n <> 1n <> (4n+p) <> Nil{}:
2814      Empty.absurd(Facts<4n, 3n <> 0n <> 1n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(3n <> 0n <> 1n <> (4n+p) <> Nil{}, 4n), Axis.unique(3n <> 0n <> 1n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 3n <> 0n <> 1n <> (4n+p) <> Nil{}), accepted)))))
2815    case 3n <> 0n <> 2n <> 0n <> Nil{}:
2816      Empty.absurd(Facts<4n, [3n, 0n, 2n, 0n]>, Shape.clash(accepted))
2817    case 3n <> 0n <> 2n <> 1n <> Nil{}:
2818      Certified{{==}, {==}, {==}, A => items => length => lists_3021(A, items, length),
2819        dims => length => product_3021(dims, length), dims => coords => dl => cl => fit_3021(dims, coords, dl, cl)}
2820    case 3n <> 0n <> 2n <> 2n <> Nil{}:
2821      Empty.absurd(Facts<4n, [3n, 0n, 2n, 2n]>, Shape.clash(accepted))
2822    case 3n <> 0n <> 2n <> 3n <> Nil{}:
2823      Empty.absurd(Facts<4n, [3n, 0n, 2n, 3n]>, Shape.clash(accepted))
2824    case 3n <> 0n <> 2n <> (4n+p) <> Nil{}:
2825      Empty.absurd(Facts<4n, 3n <> 0n <> 2n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(3n <> 0n <> 2n <> (4n+p) <> Nil{}, 4n), Axis.unique(3n <> 0n <> 2n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 3n <> 0n <> 2n <> (4n+p) <> Nil{}), accepted)))))
2826    case 3n <> 0n <> 3n <> 0n <> Nil{}:
2827      Empty.absurd(Facts<4n, [3n, 0n, 3n, 0n]>, Shape.clash(accepted))
2828    case 3n <> 0n <> 3n <> 1n <> Nil{}:
2829      Empty.absurd(Facts<4n, [3n, 0n, 3n, 1n]>, Shape.clash(accepted))
2830    case 3n <> 0n <> 3n <> 2n <> Nil{}:
2831      Empty.absurd(Facts<4n, [3n, 0n, 3n, 2n]>, Shape.clash(accepted))
2832    case 3n <> 0n <> 3n <> 3n <> Nil{}:
2833      Empty.absurd(Facts<4n, [3n, 0n, 3n, 3n]>, Shape.clash(accepted))
2834    case 3n <> 0n <> 3n <> (4n+p) <> Nil{}:
2835      Empty.absurd(Facts<4n, 3n <> 0n <> 3n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(3n <> 0n <> 3n <> (4n+p) <> Nil{}, 4n), Axis.unique(3n <> 0n <> 3n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 3n <> 0n <> 3n <> (4n+p) <> Nil{}), accepted)))))
2836    case 3n <> 0n <> (4n+p) <> a0 <> Nil{}:
2837      Empty.absurd(Facts<4n, 3n <> 0n <> (4n+p) <> a0 <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(a0 <> Nil{}, 4n), Arith.and_left(Axis.bounded(3n <> 0n <> (4n+p) <> a0 <> Nil{}, 4n), Axis.unique(3n <> 0n <> (4n+p) <> a0 <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 3n <> 0n <> (4n+p) <> a0 <> Nil{}), accepted)))))
2838    case 3n <> 1n <> 0n <> 0n <> Nil{}:
2839      Empty.absurd(Facts<4n, [3n, 1n, 0n, 0n]>, Shape.clash(accepted))
2840    case 3n <> 1n <> 0n <> 1n <> Nil{}:
2841      Empty.absurd(Facts<4n, [3n, 1n, 0n, 1n]>, Shape.clash(accepted))
2842    case 3n <> 1n <> 0n <> 2n <> Nil{}:
2843      Certified{{==}, {==}, {==}, A => items => length => lists_3102(A, items, length),
2844        dims => length => product_3102(dims, length), dims => coords => dl => cl => fit_3102(dims, coords, dl, cl)}
2845    case 3n <> 1n <> 0n <> 3n <> Nil{}:
2846      Empty.absurd(Facts<4n, [3n, 1n, 0n, 3n]>, Shape.clash(accepted))
2847    case 3n <> 1n <> 0n <> (4n+p) <> Nil{}:
2848      Empty.absurd(Facts<4n, 3n <> 1n <> 0n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(3n <> 1n <> 0n <> (4n+p) <> Nil{}, 4n), Axis.unique(3n <> 1n <> 0n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 3n <> 1n <> 0n <> (4n+p) <> Nil{}), accepted)))))
2849    case 3n <> 1n <> 1n <> 0n <> Nil{}:
2850      Empty.absurd(Facts<4n, [3n, 1n, 1n, 0n]>, Shape.clash(accepted))
2851    case 3n <> 1n <> 1n <> 1n <> Nil{}:
2852      Empty.absurd(Facts<4n, [3n, 1n, 1n, 1n]>, Shape.clash(accepted))
2853    case 3n <> 1n <> 1n <> 2n <> Nil{}:
2854      Empty.absurd(Facts<4n, [3n, 1n, 1n, 2n]>, Shape.clash(accepted))
2855    case 3n <> 1n <> 1n <> 3n <> Nil{}:
2856      Empty.absurd(Facts<4n, [3n, 1n, 1n, 3n]>, Shape.clash(accepted))
2857    case 3n <> 1n <> 1n <> (4n+p) <> Nil{}:
2858      Empty.absurd(Facts<4n, 3n <> 1n <> 1n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(3n <> 1n <> 1n <> (4n+p) <> Nil{}, 4n), Axis.unique(3n <> 1n <> 1n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 3n <> 1n <> 1n <> (4n+p) <> Nil{}), accepted)))))
2859    case 3n <> 1n <> 2n <> 0n <> Nil{}:
2860      Certified{{==}, {==}, {==}, A => items => length => lists_3120(A, items, length),
2861        dims => length => product_3120(dims, length), dims => coords => dl => cl => fit_3120(dims, coords, dl, cl)}
2862    case 3n <> 1n <> 2n <> 1n <> Nil{}:
2863      Empty.absurd(Facts<4n, [3n, 1n, 2n, 1n]>, Shape.clash(accepted))
2864    case 3n <> 1n <> 2n <> 2n <> Nil{}:
2865      Empty.absurd(Facts<4n, [3n, 1n, 2n, 2n]>, Shape.clash(accepted))
2866    case 3n <> 1n <> 2n <> 3n <> Nil{}:
2867      Empty.absurd(Facts<4n, [3n, 1n, 2n, 3n]>, Shape.clash(accepted))
2868    case 3n <> 1n <> 2n <> (4n+p) <> Nil{}:
2869      Empty.absurd(Facts<4n, 3n <> 1n <> 2n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(3n <> 1n <> 2n <> (4n+p) <> Nil{}, 4n), Axis.unique(3n <> 1n <> 2n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 3n <> 1n <> 2n <> (4n+p) <> Nil{}), accepted)))))
2870    case 3n <> 1n <> 3n <> 0n <> Nil{}:
2871      Empty.absurd(Facts<4n, [3n, 1n, 3n, 0n]>, Shape.clash(accepted))
2872    case 3n <> 1n <> 3n <> 1n <> Nil{}:
2873      Empty.absurd(Facts<4n, [3n, 1n, 3n, 1n]>, Shape.clash(accepted))
2874    case 3n <> 1n <> 3n <> 2n <> Nil{}:
2875      Empty.absurd(Facts<4n, [3n, 1n, 3n, 2n]>, Shape.clash(accepted))
2876    case 3n <> 1n <> 3n <> 3n <> Nil{}:
2877      Empty.absurd(Facts<4n, [3n, 1n, 3n, 3n]>, Shape.clash(accepted))
2878    case 3n <> 1n <> 3n <> (4n+p) <> Nil{}:
2879      Empty.absurd(Facts<4n, 3n <> 1n <> 3n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(3n <> 1n <> 3n <> (4n+p) <> Nil{}, 4n), Axis.unique(3n <> 1n <> 3n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 3n <> 1n <> 3n <> (4n+p) <> Nil{}), accepted)))))
2880    case 3n <> 1n <> (4n+p) <> a0 <> Nil{}:
2881      Empty.absurd(Facts<4n, 3n <> 1n <> (4n+p) <> a0 <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(a0 <> Nil{}, 4n), Arith.and_left(Axis.bounded(3n <> 1n <> (4n+p) <> a0 <> Nil{}, 4n), Axis.unique(3n <> 1n <> (4n+p) <> a0 <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 3n <> 1n <> (4n+p) <> a0 <> Nil{}), accepted)))))
2882    case 3n <> 2n <> 0n <> 0n <> Nil{}:
2883      Empty.absurd(Facts<4n, [3n, 2n, 0n, 0n]>, Shape.clash(accepted))
2884    case 3n <> 2n <> 0n <> 1n <> Nil{}:
2885      Certified{{==}, {==}, {==}, A => items => length => lists_3201(A, items, length),
2886        dims => length => product_3201(dims, length), dims => coords => dl => cl => fit_3201(dims, coords, dl, cl)}
2887    case 3n <> 2n <> 0n <> 2n <> Nil{}:
2888      Empty.absurd(Facts<4n, [3n, 2n, 0n, 2n]>, Shape.clash(accepted))
2889    case 3n <> 2n <> 0n <> 3n <> Nil{}:
2890      Empty.absurd(Facts<4n, [3n, 2n, 0n, 3n]>, Shape.clash(accepted))
2891    case 3n <> 2n <> 0n <> (4n+p) <> Nil{}:
2892      Empty.absurd(Facts<4n, 3n <> 2n <> 0n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(3n <> 2n <> 0n <> (4n+p) <> Nil{}, 4n), Axis.unique(3n <> 2n <> 0n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 3n <> 2n <> 0n <> (4n+p) <> Nil{}), accepted)))))
2893    case 3n <> 2n <> 1n <> 0n <> Nil{}:
2894      Certified{{==}, {==}, {==}, A => items => length => lists_3210(A, items, length),
2895        dims => length => product_3210(dims, length), dims => coords => dl => cl => fit_3210(dims, coords, dl, cl)}
2896    case 3n <> 2n <> 1n <> 1n <> Nil{}:
2897      Empty.absurd(Facts<4n, [3n, 2n, 1n, 1n]>, Shape.clash(accepted))
2898    case 3n <> 2n <> 1n <> 2n <> Nil{}:
2899      Empty.absurd(Facts<4n, [3n, 2n, 1n, 2n]>, Shape.clash(accepted))
2900    case 3n <> 2n <> 1n <> 3n <> Nil{}:
2901      Empty.absurd(Facts<4n, [3n, 2n, 1n, 3n]>, Shape.clash(accepted))
2902    case 3n <> 2n <> 1n <> (4n+p) <> Nil{}:
2903      Empty.absurd(Facts<4n, 3n <> 2n <> 1n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(3n <> 2n <> 1n <> (4n+p) <> Nil{}, 4n), Axis.unique(3n <> 2n <> 1n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 3n <> 2n <> 1n <> (4n+p) <> Nil{}), accepted)))))
2904    case 3n <> 2n <> 2n <> 0n <> Nil{}:
2905      Empty.absurd(Facts<4n, [3n, 2n, 2n, 0n]>, Shape.clash(accepted))
2906    case 3n <> 2n <> 2n <> 1n <> Nil{}:
2907      Empty.absurd(Facts<4n, [3n, 2n, 2n, 1n]>, Shape.clash(accepted))
2908    case 3n <> 2n <> 2n <> 2n <> Nil{}:
2909      Empty.absurd(Facts<4n, [3n, 2n, 2n, 2n]>, Shape.clash(accepted))
2910    case 3n <> 2n <> 2n <> 3n <> Nil{}:
2911      Empty.absurd(Facts<4n, [3n, 2n, 2n, 3n]>, Shape.clash(accepted))
2912    case 3n <> 2n <> 2n <> (4n+p) <> Nil{}:
2913      Empty.absurd(Facts<4n, 3n <> 2n <> 2n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(3n <> 2n <> 2n <> (4n+p) <> Nil{}, 4n), Axis.unique(3n <> 2n <> 2n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 3n <> 2n <> 2n <> (4n+p) <> Nil{}), accepted)))))
2914    case 3n <> 2n <> 3n <> 0n <> Nil{}:
2915      Empty.absurd(Facts<4n, [3n, 2n, 3n, 0n]>, Shape.clash(accepted))
2916    case 3n <> 2n <> 3n <> 1n <> Nil{}:
2917      Empty.absurd(Facts<4n, [3n, 2n, 3n, 1n]>, Shape.clash(accepted))
2918    case 3n <> 2n <> 3n <> 2n <> Nil{}:
2919      Empty.absurd(Facts<4n, [3n, 2n, 3n, 2n]>, Shape.clash(accepted))
2920    case 3n <> 2n <> 3n <> 3n <> Nil{}:
2921      Empty.absurd(Facts<4n, [3n, 2n, 3n, 3n]>, Shape.clash(accepted))
2922    case 3n <> 2n <> 3n <> (4n+p) <> Nil{}:
2923      Empty.absurd(Facts<4n, 3n <> 2n <> 3n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(3n <> 2n <> 3n <> (4n+p) <> Nil{}, 4n), Axis.unique(3n <> 2n <> 3n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 3n <> 2n <> 3n <> (4n+p) <> Nil{}), accepted)))))
2924    case 3n <> 2n <> (4n+p) <> a0 <> Nil{}:
2925      Empty.absurd(Facts<4n, 3n <> 2n <> (4n+p) <> a0 <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(a0 <> Nil{}, 4n), Arith.and_left(Axis.bounded(3n <> 2n <> (4n+p) <> a0 <> Nil{}, 4n), Axis.unique(3n <> 2n <> (4n+p) <> a0 <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 3n <> 2n <> (4n+p) <> a0 <> Nil{}), accepted)))))
2926    case 3n <> 3n <> 0n <> 0n <> Nil{}:
2927      Empty.absurd(Facts<4n, [3n, 3n, 0n, 0n]>, Shape.clash(accepted))
2928    case 3n <> 3n <> 0n <> 1n <> Nil{}:
2929      Empty.absurd(Facts<4n, [3n, 3n, 0n, 1n]>, Shape.clash(accepted))
2930    case 3n <> 3n <> 0n <> 2n <> Nil{}:
2931      Empty.absurd(Facts<4n, [3n, 3n, 0n, 2n]>, Shape.clash(accepted))
2932    case 3n <> 3n <> 0n <> 3n <> Nil{}:
2933      Empty.absurd(Facts<4n, [3n, 3n, 0n, 3n]>, Shape.clash(accepted))
2934    case 3n <> 3n <> 0n <> (4n+p) <> Nil{}:
2935      Empty.absurd(Facts<4n, 3n <> 3n <> 0n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(3n <> 3n <> 0n <> (4n+p) <> Nil{}, 4n), Axis.unique(3n <> 3n <> 0n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 3n <> 3n <> 0n <> (4n+p) <> Nil{}), accepted)))))
2936    case 3n <> 3n <> 1n <> 0n <> Nil{}:
2937      Empty.absurd(Facts<4n, [3n, 3n, 1n, 0n]>, Shape.clash(accepted))
2938    case 3n <> 3n <> 1n <> 1n <> Nil{}:
2939      Empty.absurd(Facts<4n, [3n, 3n, 1n, 1n]>, Shape.clash(accepted))
2940    case 3n <> 3n <> 1n <> 2n <> Nil{}:
2941      Empty.absurd(Facts<4n, [3n, 3n, 1n, 2n]>, Shape.clash(accepted))
2942    case 3n <> 3n <> 1n <> 3n <> Nil{}:
2943      Empty.absurd(Facts<4n, [3n, 3n, 1n, 3n]>, Shape.clash(accepted))
2944    case 3n <> 3n <> 1n <> (4n+p) <> Nil{}:
2945      Empty.absurd(Facts<4n, 3n <> 3n <> 1n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(3n <> 3n <> 1n <> (4n+p) <> Nil{}, 4n), Axis.unique(3n <> 3n <> 1n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 3n <> 3n <> 1n <> (4n+p) <> Nil{}), accepted)))))
2946    case 3n <> 3n <> 2n <> 0n <> Nil{}:
2947      Empty.absurd(Facts<4n, [3n, 3n, 2n, 0n]>, Shape.clash(accepted))
2948    case 3n <> 3n <> 2n <> 1n <> Nil{}:
2949      Empty.absurd(Facts<4n, [3n, 3n, 2n, 1n]>, Shape.clash(accepted))
2950    case 3n <> 3n <> 2n <> 2n <> Nil{}:
2951      Empty.absurd(Facts<4n, [3n, 3n, 2n, 2n]>, Shape.clash(accepted))
2952    case 3n <> 3n <> 2n <> 3n <> Nil{}:
2953      Empty.absurd(Facts<4n, [3n, 3n, 2n, 3n]>, Shape.clash(accepted))
2954    case 3n <> 3n <> 2n <> (4n+p) <> Nil{}:
2955      Empty.absurd(Facts<4n, 3n <> 3n <> 2n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(3n <> 3n <> 2n <> (4n+p) <> Nil{}, 4n), Axis.unique(3n <> 3n <> 2n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 3n <> 3n <> 2n <> (4n+p) <> Nil{}), accepted)))))
2956    case 3n <> 3n <> 3n <> 0n <> Nil{}:
2957      Empty.absurd(Facts<4n, [3n, 3n, 3n, 0n]>, Shape.clash(accepted))
2958    case 3n <> 3n <> 3n <> 1n <> Nil{}:
2959      Empty.absurd(Facts<4n, [3n, 3n, 3n, 1n]>, Shape.clash(accepted))
2960    case 3n <> 3n <> 3n <> 2n <> Nil{}:
2961      Empty.absurd(Facts<4n, [3n, 3n, 3n, 2n]>, Shape.clash(accepted))
2962    case 3n <> 3n <> 3n <> 3n <> Nil{}:
2963      Empty.absurd(Facts<4n, [3n, 3n, 3n, 3n]>, Shape.clash(accepted))
2964    case 3n <> 3n <> 3n <> (4n+p) <> Nil{}:
2965      Empty.absurd(Facts<4n, 3n <> 3n <> 3n <> (4n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(Nil{}, 4n), Arith.and_left(Axis.bounded(3n <> 3n <> 3n <> (4n+p) <> Nil{}, 4n), Axis.unique(3n <> 3n <> 3n <> (4n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 3n <> 3n <> 3n <> (4n+p) <> Nil{}), accepted)))))
2966    case 3n <> 3n <> (4n+p) <> a0 <> Nil{}:
2967      Empty.absurd(Facts<4n, 3n <> 3n <> (4n+p) <> a0 <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(a0 <> Nil{}, 4n), Arith.and_left(Axis.bounded(3n <> 3n <> (4n+p) <> a0 <> Nil{}, 4n), Axis.unique(3n <> 3n <> (4n+p) <> a0 <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 3n <> 3n <> (4n+p) <> a0 <> Nil{}), accepted)))))
2968    case 3n <> (4n+p) <> a0 <> a1 <> Nil{}:
2969      Empty.absurd(Facts<4n, 3n <> (4n+p) <> a0 <> a1 <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(a0 <> a1 <> Nil{}, 4n), Arith.and_left(Axis.bounded(3n <> (4n+p) <> a0 <> a1 <> Nil{}, 4n), Axis.unique(3n <> (4n+p) <> a0 <> a1 <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, 3n <> (4n+p) <> a0 <> a1 <> Nil{}), accepted)))))
2970    case (4n+p) <> a0 <> a1 <> a2 <> Nil{}:
2971      Empty.absurd(Facts<4n, (4n+p) <> a0 <> a1 <> a2 <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Axis.bounded(a0 <> a1 <> a2 <> Nil{}, 4n), Arith.and_left(Axis.bounded((4n+p) <> a0 <> a1 <> a2 <> Nil{}, 4n), Axis.unique((4n+p) <> a0 <> a1 <> a2 <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(4n, (4n+p) <> a0 <> a1 <> a2 <> Nil{}), accepted)))))
2972    case +a0 <> +a1 <> +a2 <> +a3 <> +a4 <> +tail:
2973      Empty.absurd(Facts<4n, a0 <> a1 <> a2 <> a3 <> a4 <> tail>, Shape.clash(accepted))