AxisAlgebra.facts_4: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend as AxisAlgebra
Lines 2256-2973 of bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&start_line=2256&end_line=2973

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

def facts_4(+axes: List<&2, Nat>, accepted: {True{} == Axis.valid(4n, axes) : Bool}) -> Facts<4n, axes>:
  match axes:
    case Nil{}:
      Empty.absurd(Facts<4n, Nil{}>, Shape.clash(accepted))
    case +a0 <> Nil{}:
      Empty.absurd(Facts<4n, a0 <> Nil{}>, Shape.clash(accepted))
    case +a0 <> +a1 <> Nil{}:
      Empty.absurd(Facts<4n, a0 <> a1 <> Nil{}>, Shape.clash(accepted))
    case +a0 <> +a1 <> +a2 <> Nil{}:
      Empty.absurd(Facts<4n, a0 <> a1 <> a2 <> Nil{}>, Shape.clash(accepted))
    case 0n <> 0n <> 0n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 0n, 0n, 0n]>, Shape.clash(accepted))
    case 0n <> 0n <> 0n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 0n, 0n, 1n]>, Shape.clash(accepted))
    case 0n <> 0n <> 0n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 0n, 0n, 2n]>, Shape.clash(accepted))
    case 0n <> 0n <> 0n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 0n, 0n, 3n]>, Shape.clash(accepted))
    case 0n <> 0n <> 0n <> (4n+p) <> Nil{}:
      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)))))
    case 0n <> 0n <> 1n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 0n, 1n, 0n]>, Shape.clash(accepted))
    case 0n <> 0n <> 1n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 0n, 1n, 1n]>, Shape.clash(accepted))
    case 0n <> 0n <> 1n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 0n, 1n, 2n]>, Shape.clash(accepted))
    case 0n <> 0n <> 1n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 0n, 1n, 3n]>, Shape.clash(accepted))
    case 0n <> 0n <> 1n <> (4n+p) <> Nil{}:
      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)))))
    case 0n <> 0n <> 2n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 0n, 2n, 0n]>, Shape.clash(accepted))
    case 0n <> 0n <> 2n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 0n, 2n, 1n]>, Shape.clash(accepted))
    case 0n <> 0n <> 2n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 0n, 2n, 2n]>, Shape.clash(accepted))
    case 0n <> 0n <> 2n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 0n, 2n, 3n]>, Shape.clash(accepted))
    case 0n <> 0n <> 2n <> (4n+p) <> Nil{}:
      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)))))
    case 0n <> 0n <> 3n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 0n, 3n, 0n]>, Shape.clash(accepted))
    case 0n <> 0n <> 3n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 0n, 3n, 1n]>, Shape.clash(accepted))
    case 0n <> 0n <> 3n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 0n, 3n, 2n]>, Shape.clash(accepted))
    case 0n <> 0n <> 3n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 0n, 3n, 3n]>, Shape.clash(accepted))
    case 0n <> 0n <> 3n <> (4n+p) <> Nil{}:
      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)))))
    case 0n <> 0n <> (4n+p) <> a0 <> Nil{}:
      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)))))
    case 0n <> 1n <> 0n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 1n, 0n, 0n]>, Shape.clash(accepted))
    case 0n <> 1n <> 0n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 1n, 0n, 1n]>, Shape.clash(accepted))
    case 0n <> 1n <> 0n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 1n, 0n, 2n]>, Shape.clash(accepted))
    case 0n <> 1n <> 0n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 1n, 0n, 3n]>, Shape.clash(accepted))
    case 0n <> 1n <> 0n <> (4n+p) <> Nil{}:
      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)))))
    case 0n <> 1n <> 1n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 1n, 1n, 0n]>, Shape.clash(accepted))
    case 0n <> 1n <> 1n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 1n, 1n, 1n]>, Shape.clash(accepted))
    case 0n <> 1n <> 1n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 1n, 1n, 2n]>, Shape.clash(accepted))
    case 0n <> 1n <> 1n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 1n, 1n, 3n]>, Shape.clash(accepted))
    case 0n <> 1n <> 1n <> (4n+p) <> Nil{}:
      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)))))
    case 0n <> 1n <> 2n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 1n, 2n, 0n]>, Shape.clash(accepted))
    case 0n <> 1n <> 2n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 1n, 2n, 1n]>, Shape.clash(accepted))
    case 0n <> 1n <> 2n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 1n, 2n, 2n]>, Shape.clash(accepted))
    case 0n <> 1n <> 2n <> 3n <> Nil{}:
      Certified{{==}, {==}, {==}, A => items => length => lists_0123(A, items, length),
        dims => length => product_0123(dims, length), dims => coords => dl => cl => fit_0123(dims, coords, dl, cl)}
    case 0n <> 1n <> 2n <> (4n+p) <> Nil{}:
      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)))))
    case 0n <> 1n <> 3n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 1n, 3n, 0n]>, Shape.clash(accepted))
    case 0n <> 1n <> 3n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 1n, 3n, 1n]>, Shape.clash(accepted))
    case 0n <> 1n <> 3n <> 2n <> Nil{}:
      Certified{{==}, {==}, {==}, A => items => length => lists_0132(A, items, length),
        dims => length => product_0132(dims, length), dims => coords => dl => cl => fit_0132(dims, coords, dl, cl)}
    case 0n <> 1n <> 3n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 1n, 3n, 3n]>, Shape.clash(accepted))
    case 0n <> 1n <> 3n <> (4n+p) <> Nil{}:
      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)))))
    case 0n <> 1n <> (4n+p) <> a0 <> Nil{}:
      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)))))
    case 0n <> 2n <> 0n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 2n, 0n, 0n]>, Shape.clash(accepted))
    case 0n <> 2n <> 0n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 2n, 0n, 1n]>, Shape.clash(accepted))
    case 0n <> 2n <> 0n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 2n, 0n, 2n]>, Shape.clash(accepted))
    case 0n <> 2n <> 0n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 2n, 0n, 3n]>, Shape.clash(accepted))
    case 0n <> 2n <> 0n <> (4n+p) <> Nil{}:
      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)))))
    case 0n <> 2n <> 1n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 2n, 1n, 0n]>, Shape.clash(accepted))
    case 0n <> 2n <> 1n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 2n, 1n, 1n]>, Shape.clash(accepted))
    case 0n <> 2n <> 1n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 2n, 1n, 2n]>, Shape.clash(accepted))
    case 0n <> 2n <> 1n <> 3n <> Nil{}:
      Certified{{==}, {==}, {==}, A => items => length => lists_0213(A, items, length),
        dims => length => product_0213(dims, length), dims => coords => dl => cl => fit_0213(dims, coords, dl, cl)}
    case 0n <> 2n <> 1n <> (4n+p) <> Nil{}:
      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)))))
    case 0n <> 2n <> 2n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 2n, 2n, 0n]>, Shape.clash(accepted))
    case 0n <> 2n <> 2n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 2n, 2n, 1n]>, Shape.clash(accepted))
    case 0n <> 2n <> 2n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 2n, 2n, 2n]>, Shape.clash(accepted))
    case 0n <> 2n <> 2n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 2n, 2n, 3n]>, Shape.clash(accepted))
    case 0n <> 2n <> 2n <> (4n+p) <> Nil{}:
      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)))))
    case 0n <> 2n <> 3n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 2n, 3n, 0n]>, Shape.clash(accepted))
    case 0n <> 2n <> 3n <> 1n <> Nil{}:
      Certified{{==}, {==}, {==}, A => items => length => lists_0231(A, items, length),
        dims => length => product_0231(dims, length), dims => coords => dl => cl => fit_0231(dims, coords, dl, cl)}
    case 0n <> 2n <> 3n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 2n, 3n, 2n]>, Shape.clash(accepted))
    case 0n <> 2n <> 3n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 2n, 3n, 3n]>, Shape.clash(accepted))
    case 0n <> 2n <> 3n <> (4n+p) <> Nil{}:
      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)))))
    case 0n <> 2n <> (4n+p) <> a0 <> Nil{}:
      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)))))
    case 0n <> 3n <> 0n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 3n, 0n, 0n]>, Shape.clash(accepted))
    case 0n <> 3n <> 0n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 3n, 0n, 1n]>, Shape.clash(accepted))
    case 0n <> 3n <> 0n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 3n, 0n, 2n]>, Shape.clash(accepted))
    case 0n <> 3n <> 0n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 3n, 0n, 3n]>, Shape.clash(accepted))
    case 0n <> 3n <> 0n <> (4n+p) <> Nil{}:
      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)))))
    case 0n <> 3n <> 1n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 3n, 1n, 0n]>, Shape.clash(accepted))
    case 0n <> 3n <> 1n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 3n, 1n, 1n]>, Shape.clash(accepted))
    case 0n <> 3n <> 1n <> 2n <> Nil{}:
      Certified{{==}, {==}, {==}, A => items => length => lists_0312(A, items, length),
        dims => length => product_0312(dims, length), dims => coords => dl => cl => fit_0312(dims, coords, dl, cl)}
    case 0n <> 3n <> 1n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 3n, 1n, 3n]>, Shape.clash(accepted))
    case 0n <> 3n <> 1n <> (4n+p) <> Nil{}:
      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)))))
    case 0n <> 3n <> 2n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 3n, 2n, 0n]>, Shape.clash(accepted))
    case 0n <> 3n <> 2n <> 1n <> Nil{}:
      Certified{{==}, {==}, {==}, A => items => length => lists_0321(A, items, length),
        dims => length => product_0321(dims, length), dims => coords => dl => cl => fit_0321(dims, coords, dl, cl)}
    case 0n <> 3n <> 2n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 3n, 2n, 2n]>, Shape.clash(accepted))
    case 0n <> 3n <> 2n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 3n, 2n, 3n]>, Shape.clash(accepted))
    case 0n <> 3n <> 2n <> (4n+p) <> Nil{}:
      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)))))
    case 0n <> 3n <> 3n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 3n, 3n, 0n]>, Shape.clash(accepted))
    case 0n <> 3n <> 3n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 3n, 3n, 1n]>, Shape.clash(accepted))
    case 0n <> 3n <> 3n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 3n, 3n, 2n]>, Shape.clash(accepted))
    case 0n <> 3n <> 3n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [0n, 3n, 3n, 3n]>, Shape.clash(accepted))
    case 0n <> 3n <> 3n <> (4n+p) <> Nil{}:
      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)))))
    case 0n <> 3n <> (4n+p) <> a0 <> Nil{}:
      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)))))
    case 0n <> (4n+p) <> a0 <> a1 <> Nil{}:
      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)))))
    case 1n <> 0n <> 0n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 0n, 0n, 0n]>, Shape.clash(accepted))
    case 1n <> 0n <> 0n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 0n, 0n, 1n]>, Shape.clash(accepted))
    case 1n <> 0n <> 0n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 0n, 0n, 2n]>, Shape.clash(accepted))
    case 1n <> 0n <> 0n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 0n, 0n, 3n]>, Shape.clash(accepted))
    case 1n <> 0n <> 0n <> (4n+p) <> Nil{}:
      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)))))
    case 1n <> 0n <> 1n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 0n, 1n, 0n]>, Shape.clash(accepted))
    case 1n <> 0n <> 1n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 0n, 1n, 1n]>, Shape.clash(accepted))
    case 1n <> 0n <> 1n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 0n, 1n, 2n]>, Shape.clash(accepted))
    case 1n <> 0n <> 1n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 0n, 1n, 3n]>, Shape.clash(accepted))
    case 1n <> 0n <> 1n <> (4n+p) <> Nil{}:
      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)))))
    case 1n <> 0n <> 2n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 0n, 2n, 0n]>, Shape.clash(accepted))
    case 1n <> 0n <> 2n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 0n, 2n, 1n]>, Shape.clash(accepted))
    case 1n <> 0n <> 2n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 0n, 2n, 2n]>, Shape.clash(accepted))
    case 1n <> 0n <> 2n <> 3n <> Nil{}:
      Certified{{==}, {==}, {==}, A => items => length => lists_1023(A, items, length),
        dims => length => product_1023(dims, length), dims => coords => dl => cl => fit_1023(dims, coords, dl, cl)}
    case 1n <> 0n <> 2n <> (4n+p) <> Nil{}:
      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)))))
    case 1n <> 0n <> 3n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 0n, 3n, 0n]>, Shape.clash(accepted))
    case 1n <> 0n <> 3n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 0n, 3n, 1n]>, Shape.clash(accepted))
    case 1n <> 0n <> 3n <> 2n <> Nil{}:
      Certified{{==}, {==}, {==}, A => items => length => lists_1032(A, items, length),
        dims => length => product_1032(dims, length), dims => coords => dl => cl => fit_1032(dims, coords, dl, cl)}
    case 1n <> 0n <> 3n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 0n, 3n, 3n]>, Shape.clash(accepted))
    case 1n <> 0n <> 3n <> (4n+p) <> Nil{}:
      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)))))
    case 1n <> 0n <> (4n+p) <> a0 <> Nil{}:
      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)))))
    case 1n <> 1n <> 0n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 1n, 0n, 0n]>, Shape.clash(accepted))
    case 1n <> 1n <> 0n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 1n, 0n, 1n]>, Shape.clash(accepted))
    case 1n <> 1n <> 0n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 1n, 0n, 2n]>, Shape.clash(accepted))
    case 1n <> 1n <> 0n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 1n, 0n, 3n]>, Shape.clash(accepted))
    case 1n <> 1n <> 0n <> (4n+p) <> Nil{}:
      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)))))
    case 1n <> 1n <> 1n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 1n, 1n, 0n]>, Shape.clash(accepted))
    case 1n <> 1n <> 1n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 1n, 1n, 1n]>, Shape.clash(accepted))
    case 1n <> 1n <> 1n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 1n, 1n, 2n]>, Shape.clash(accepted))
    case 1n <> 1n <> 1n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 1n, 1n, 3n]>, Shape.clash(accepted))
    case 1n <> 1n <> 1n <> (4n+p) <> Nil{}:
      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)))))
    case 1n <> 1n <> 2n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 1n, 2n, 0n]>, Shape.clash(accepted))
    case 1n <> 1n <> 2n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 1n, 2n, 1n]>, Shape.clash(accepted))
    case 1n <> 1n <> 2n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 1n, 2n, 2n]>, Shape.clash(accepted))
    case 1n <> 1n <> 2n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 1n, 2n, 3n]>, Shape.clash(accepted))
    case 1n <> 1n <> 2n <> (4n+p) <> Nil{}:
      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)))))
    case 1n <> 1n <> 3n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 1n, 3n, 0n]>, Shape.clash(accepted))
    case 1n <> 1n <> 3n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 1n, 3n, 1n]>, Shape.clash(accepted))
    case 1n <> 1n <> 3n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 1n, 3n, 2n]>, Shape.clash(accepted))
    case 1n <> 1n <> 3n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 1n, 3n, 3n]>, Shape.clash(accepted))
    case 1n <> 1n <> 3n <> (4n+p) <> Nil{}:
      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)))))
    case 1n <> 1n <> (4n+p) <> a0 <> Nil{}:
      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)))))
    case 1n <> 2n <> 0n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 2n, 0n, 0n]>, Shape.clash(accepted))
    case 1n <> 2n <> 0n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 2n, 0n, 1n]>, Shape.clash(accepted))
    case 1n <> 2n <> 0n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 2n, 0n, 2n]>, Shape.clash(accepted))
    case 1n <> 2n <> 0n <> 3n <> Nil{}:
      Certified{{==}, {==}, {==}, A => items => length => lists_1203(A, items, length),
        dims => length => product_1203(dims, length), dims => coords => dl => cl => fit_1203(dims, coords, dl, cl)}
    case 1n <> 2n <> 0n <> (4n+p) <> Nil{}:
      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)))))
    case 1n <> 2n <> 1n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 2n, 1n, 0n]>, Shape.clash(accepted))
    case 1n <> 2n <> 1n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 2n, 1n, 1n]>, Shape.clash(accepted))
    case 1n <> 2n <> 1n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 2n, 1n, 2n]>, Shape.clash(accepted))
    case 1n <> 2n <> 1n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 2n, 1n, 3n]>, Shape.clash(accepted))
    case 1n <> 2n <> 1n <> (4n+p) <> Nil{}:
      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)))))
    case 1n <> 2n <> 2n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 2n, 2n, 0n]>, Shape.clash(accepted))
    case 1n <> 2n <> 2n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 2n, 2n, 1n]>, Shape.clash(accepted))
    case 1n <> 2n <> 2n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 2n, 2n, 2n]>, Shape.clash(accepted))
    case 1n <> 2n <> 2n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 2n, 2n, 3n]>, Shape.clash(accepted))
    case 1n <> 2n <> 2n <> (4n+p) <> Nil{}:
      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)))))
    case 1n <> 2n <> 3n <> 0n <> Nil{}:
      Certified{{==}, {==}, {==}, A => items => length => lists_1230(A, items, length),
        dims => length => product_1230(dims, length), dims => coords => dl => cl => fit_1230(dims, coords, dl, cl)}
    case 1n <> 2n <> 3n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 2n, 3n, 1n]>, Shape.clash(accepted))
    case 1n <> 2n <> 3n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 2n, 3n, 2n]>, Shape.clash(accepted))
    case 1n <> 2n <> 3n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 2n, 3n, 3n]>, Shape.clash(accepted))
    case 1n <> 2n <> 3n <> (4n+p) <> Nil{}:
      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)))))
    case 1n <> 2n <> (4n+p) <> a0 <> Nil{}:
      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)))))
    case 1n <> 3n <> 0n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 3n, 0n, 0n]>, Shape.clash(accepted))
    case 1n <> 3n <> 0n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 3n, 0n, 1n]>, Shape.clash(accepted))
    case 1n <> 3n <> 0n <> 2n <> Nil{}:
      Certified{{==}, {==}, {==}, A => items => length => lists_1302(A, items, length),
        dims => length => product_1302(dims, length), dims => coords => dl => cl => fit_1302(dims, coords, dl, cl)}
    case 1n <> 3n <> 0n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 3n, 0n, 3n]>, Shape.clash(accepted))
    case 1n <> 3n <> 0n <> (4n+p) <> Nil{}:
      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)))))
    case 1n <> 3n <> 1n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 3n, 1n, 0n]>, Shape.clash(accepted))
    case 1n <> 3n <> 1n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 3n, 1n, 1n]>, Shape.clash(accepted))
    case 1n <> 3n <> 1n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 3n, 1n, 2n]>, Shape.clash(accepted))
    case 1n <> 3n <> 1n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 3n, 1n, 3n]>, Shape.clash(accepted))
    case 1n <> 3n <> 1n <> (4n+p) <> Nil{}:
      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)))))
    case 1n <> 3n <> 2n <> 0n <> Nil{}:
      Certified{{==}, {==}, {==}, A => items => length => lists_1320(A, items, length),
        dims => length => product_1320(dims, length), dims => coords => dl => cl => fit_1320(dims, coords, dl, cl)}
    case 1n <> 3n <> 2n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 3n, 2n, 1n]>, Shape.clash(accepted))
    case 1n <> 3n <> 2n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 3n, 2n, 2n]>, Shape.clash(accepted))
    case 1n <> 3n <> 2n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 3n, 2n, 3n]>, Shape.clash(accepted))
    case 1n <> 3n <> 2n <> (4n+p) <> Nil{}:
      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)))))
    case 1n <> 3n <> 3n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 3n, 3n, 0n]>, Shape.clash(accepted))
    case 1n <> 3n <> 3n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 3n, 3n, 1n]>, Shape.clash(accepted))
    case 1n <> 3n <> 3n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 3n, 3n, 2n]>, Shape.clash(accepted))
    case 1n <> 3n <> 3n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [1n, 3n, 3n, 3n]>, Shape.clash(accepted))
    case 1n <> 3n <> 3n <> (4n+p) <> Nil{}:
      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)))))
    case 1n <> 3n <> (4n+p) <> a0 <> Nil{}:
      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)))))
    case 1n <> (4n+p) <> a0 <> a1 <> Nil{}:
      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)))))
    case 2n <> 0n <> 0n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 0n, 0n, 0n]>, Shape.clash(accepted))
    case 2n <> 0n <> 0n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 0n, 0n, 1n]>, Shape.clash(accepted))
    case 2n <> 0n <> 0n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 0n, 0n, 2n]>, Shape.clash(accepted))
    case 2n <> 0n <> 0n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 0n, 0n, 3n]>, Shape.clash(accepted))
    case 2n <> 0n <> 0n <> (4n+p) <> Nil{}:
      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)))))
    case 2n <> 0n <> 1n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 0n, 1n, 0n]>, Shape.clash(accepted))
    case 2n <> 0n <> 1n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 0n, 1n, 1n]>, Shape.clash(accepted))
    case 2n <> 0n <> 1n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 0n, 1n, 2n]>, Shape.clash(accepted))
    case 2n <> 0n <> 1n <> 3n <> Nil{}:
      Certified{{==}, {==}, {==}, A => items => length => lists_2013(A, items, length),
        dims => length => product_2013(dims, length), dims => coords => dl => cl => fit_2013(dims, coords, dl, cl)}
    case 2n <> 0n <> 1n <> (4n+p) <> Nil{}:
      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)))))
    case 2n <> 0n <> 2n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 0n, 2n, 0n]>, Shape.clash(accepted))
    case 2n <> 0n <> 2n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 0n, 2n, 1n]>, Shape.clash(accepted))
    case 2n <> 0n <> 2n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 0n, 2n, 2n]>, Shape.clash(accepted))
    case 2n <> 0n <> 2n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 0n, 2n, 3n]>, Shape.clash(accepted))
    case 2n <> 0n <> 2n <> (4n+p) <> Nil{}:
      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)))))
    case 2n <> 0n <> 3n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 0n, 3n, 0n]>, Shape.clash(accepted))
    case 2n <> 0n <> 3n <> 1n <> Nil{}:
      Certified{{==}, {==}, {==}, A => items => length => lists_2031(A, items, length),
        dims => length => product_2031(dims, length), dims => coords => dl => cl => fit_2031(dims, coords, dl, cl)}
    case 2n <> 0n <> 3n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 0n, 3n, 2n]>, Shape.clash(accepted))
    case 2n <> 0n <> 3n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 0n, 3n, 3n]>, Shape.clash(accepted))
    case 2n <> 0n <> 3n <> (4n+p) <> Nil{}:
      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)))))
    case 2n <> 0n <> (4n+p) <> a0 <> Nil{}:
      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)))))
    case 2n <> 1n <> 0n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 1n, 0n, 0n]>, Shape.clash(accepted))
    case 2n <> 1n <> 0n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 1n, 0n, 1n]>, Shape.clash(accepted))
    case 2n <> 1n <> 0n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 1n, 0n, 2n]>, Shape.clash(accepted))
    case 2n <> 1n <> 0n <> 3n <> Nil{}:
      Certified{{==}, {==}, {==}, A => items => length => lists_2103(A, items, length),
        dims => length => product_2103(dims, length), dims => coords => dl => cl => fit_2103(dims, coords, dl, cl)}
    case 2n <> 1n <> 0n <> (4n+p) <> Nil{}:
      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)))))
    case 2n <> 1n <> 1n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 1n, 1n, 0n]>, Shape.clash(accepted))
    case 2n <> 1n <> 1n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 1n, 1n, 1n]>, Shape.clash(accepted))
    case 2n <> 1n <> 1n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 1n, 1n, 2n]>, Shape.clash(accepted))
    case 2n <> 1n <> 1n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 1n, 1n, 3n]>, Shape.clash(accepted))
    case 2n <> 1n <> 1n <> (4n+p) <> Nil{}:
      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)))))
    case 2n <> 1n <> 2n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 1n, 2n, 0n]>, Shape.clash(accepted))
    case 2n <> 1n <> 2n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 1n, 2n, 1n]>, Shape.clash(accepted))
    case 2n <> 1n <> 2n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 1n, 2n, 2n]>, Shape.clash(accepted))
    case 2n <> 1n <> 2n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 1n, 2n, 3n]>, Shape.clash(accepted))
    case 2n <> 1n <> 2n <> (4n+p) <> Nil{}:
      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)))))
    case 2n <> 1n <> 3n <> 0n <> Nil{}:
      Certified{{==}, {==}, {==}, A => items => length => lists_2130(A, items, length),
        dims => length => product_2130(dims, length), dims => coords => dl => cl => fit_2130(dims, coords, dl, cl)}
    case 2n <> 1n <> 3n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 1n, 3n, 1n]>, Shape.clash(accepted))
    case 2n <> 1n <> 3n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 1n, 3n, 2n]>, Shape.clash(accepted))
    case 2n <> 1n <> 3n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 1n, 3n, 3n]>, Shape.clash(accepted))
    case 2n <> 1n <> 3n <> (4n+p) <> Nil{}:
      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)))))
    case 2n <> 1n <> (4n+p) <> a0 <> Nil{}:
      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)))))
    case 2n <> 2n <> 0n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 2n, 0n, 0n]>, Shape.clash(accepted))
    case 2n <> 2n <> 0n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 2n, 0n, 1n]>, Shape.clash(accepted))
    case 2n <> 2n <> 0n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 2n, 0n, 2n]>, Shape.clash(accepted))
    case 2n <> 2n <> 0n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 2n, 0n, 3n]>, Shape.clash(accepted))
    case 2n <> 2n <> 0n <> (4n+p) <> Nil{}:
      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)))))
    case 2n <> 2n <> 1n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 2n, 1n, 0n]>, Shape.clash(accepted))
    case 2n <> 2n <> 1n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 2n, 1n, 1n]>, Shape.clash(accepted))
    case 2n <> 2n <> 1n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 2n, 1n, 2n]>, Shape.clash(accepted))
    case 2n <> 2n <> 1n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 2n, 1n, 3n]>, Shape.clash(accepted))
    case 2n <> 2n <> 1n <> (4n+p) <> Nil{}:
      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)))))
    case 2n <> 2n <> 2n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 2n, 2n, 0n]>, Shape.clash(accepted))
    case 2n <> 2n <> 2n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 2n, 2n, 1n]>, Shape.clash(accepted))
    case 2n <> 2n <> 2n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 2n, 2n, 2n]>, Shape.clash(accepted))
    case 2n <> 2n <> 2n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 2n, 2n, 3n]>, Shape.clash(accepted))
    case 2n <> 2n <> 2n <> (4n+p) <> Nil{}:
      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)))))
    case 2n <> 2n <> 3n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 2n, 3n, 0n]>, Shape.clash(accepted))
    case 2n <> 2n <> 3n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 2n, 3n, 1n]>, Shape.clash(accepted))
    case 2n <> 2n <> 3n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 2n, 3n, 2n]>, Shape.clash(accepted))
    case 2n <> 2n <> 3n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 2n, 3n, 3n]>, Shape.clash(accepted))
    case 2n <> 2n <> 3n <> (4n+p) <> Nil{}:
      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)))))
    case 2n <> 2n <> (4n+p) <> a0 <> Nil{}:
      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)))))
    case 2n <> 3n <> 0n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 3n, 0n, 0n]>, Shape.clash(accepted))
    case 2n <> 3n <> 0n <> 1n <> Nil{}:
      Certified{{==}, {==}, {==}, A => items => length => lists_2301(A, items, length),
        dims => length => product_2301(dims, length), dims => coords => dl => cl => fit_2301(dims, coords, dl, cl)}
    case 2n <> 3n <> 0n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 3n, 0n, 2n]>, Shape.clash(accepted))
    case 2n <> 3n <> 0n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 3n, 0n, 3n]>, Shape.clash(accepted))
    case 2n <> 3n <> 0n <> (4n+p) <> Nil{}:
      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)))))
    case 2n <> 3n <> 1n <> 0n <> Nil{}:
      Certified{{==}, {==}, {==}, A => items => length => lists_2310(A, items, length),
        dims => length => product_2310(dims, length), dims => coords => dl => cl => fit_2310(dims, coords, dl, cl)}
    case 2n <> 3n <> 1n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 3n, 1n, 1n]>, Shape.clash(accepted))
    case 2n <> 3n <> 1n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 3n, 1n, 2n]>, Shape.clash(accepted))
    case 2n <> 3n <> 1n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 3n, 1n, 3n]>, Shape.clash(accepted))
    case 2n <> 3n <> 1n <> (4n+p) <> Nil{}:
      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)))))
    case 2n <> 3n <> 2n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 3n, 2n, 0n]>, Shape.clash(accepted))
    case 2n <> 3n <> 2n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 3n, 2n, 1n]>, Shape.clash(accepted))
    case 2n <> 3n <> 2n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 3n, 2n, 2n]>, Shape.clash(accepted))
    case 2n <> 3n <> 2n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 3n, 2n, 3n]>, Shape.clash(accepted))
    case 2n <> 3n <> 2n <> (4n+p) <> Nil{}:
      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)))))
    case 2n <> 3n <> 3n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 3n, 3n, 0n]>, Shape.clash(accepted))
    case 2n <> 3n <> 3n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 3n, 3n, 1n]>, Shape.clash(accepted))
    case 2n <> 3n <> 3n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 3n, 3n, 2n]>, Shape.clash(accepted))
    case 2n <> 3n <> 3n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [2n, 3n, 3n, 3n]>, Shape.clash(accepted))
    case 2n <> 3n <> 3n <> (4n+p) <> Nil{}:
      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)))))
    case 2n <> 3n <> (4n+p) <> a0 <> Nil{}:
      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)))))
    case 2n <> (4n+p) <> a0 <> a1 <> Nil{}:
      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)))))
    case 3n <> 0n <> 0n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 0n, 0n, 0n]>, Shape.clash(accepted))
    case 3n <> 0n <> 0n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 0n, 0n, 1n]>, Shape.clash(accepted))
    case 3n <> 0n <> 0n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 0n, 0n, 2n]>, Shape.clash(accepted))
    case 3n <> 0n <> 0n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 0n, 0n, 3n]>, Shape.clash(accepted))
    case 3n <> 0n <> 0n <> (4n+p) <> Nil{}:
      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)))))
    case 3n <> 0n <> 1n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 0n, 1n, 0n]>, Shape.clash(accepted))
    case 3n <> 0n <> 1n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 0n, 1n, 1n]>, Shape.clash(accepted))
    case 3n <> 0n <> 1n <> 2n <> Nil{}:
      Certified{{==}, {==}, {==}, A => items => length => lists_3012(A, items, length),
        dims => length => product_3012(dims, length), dims => coords => dl => cl => fit_3012(dims, coords, dl, cl)}
    case 3n <> 0n <> 1n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 0n, 1n, 3n]>, Shape.clash(accepted))
    case 3n <> 0n <> 1n <> (4n+p) <> Nil{}:
      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)))))
    case 3n <> 0n <> 2n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 0n, 2n, 0n]>, Shape.clash(accepted))
    case 3n <> 0n <> 2n <> 1n <> Nil{}:
      Certified{{==}, {==}, {==}, A => items => length => lists_3021(A, items, length),
        dims => length => product_3021(dims, length), dims => coords => dl => cl => fit_3021(dims, coords, dl, cl)}
    case 3n <> 0n <> 2n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 0n, 2n, 2n]>, Shape.clash(accepted))
    case 3n <> 0n <> 2n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 0n, 2n, 3n]>, Shape.clash(accepted))
    case 3n <> 0n <> 2n <> (4n+p) <> Nil{}:
      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)))))
    case 3n <> 0n <> 3n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 0n, 3n, 0n]>, Shape.clash(accepted))
    case 3n <> 0n <> 3n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 0n, 3n, 1n]>, Shape.clash(accepted))
    case 3n <> 0n <> 3n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 0n, 3n, 2n]>, Shape.clash(accepted))
    case 3n <> 0n <> 3n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 0n, 3n, 3n]>, Shape.clash(accepted))
    case 3n <> 0n <> 3n <> (4n+p) <> Nil{}:
      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)))))
    case 3n <> 0n <> (4n+p) <> a0 <> Nil{}:
      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)))))
    case 3n <> 1n <> 0n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 1n, 0n, 0n]>, Shape.clash(accepted))
    case 3n <> 1n <> 0n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 1n, 0n, 1n]>, Shape.clash(accepted))
    case 3n <> 1n <> 0n <> 2n <> Nil{}:
      Certified{{==}, {==}, {==}, A => items => length => lists_3102(A, items, length),
        dims => length => product_3102(dims, length), dims => coords => dl => cl => fit_3102(dims, coords, dl, cl)}
    case 3n <> 1n <> 0n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 1n, 0n, 3n]>, Shape.clash(accepted))
    case 3n <> 1n <> 0n <> (4n+p) <> Nil{}:
      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)))))
    case 3n <> 1n <> 1n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 1n, 1n, 0n]>, Shape.clash(accepted))
    case 3n <> 1n <> 1n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 1n, 1n, 1n]>, Shape.clash(accepted))
    case 3n <> 1n <> 1n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 1n, 1n, 2n]>, Shape.clash(accepted))
    case 3n <> 1n <> 1n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 1n, 1n, 3n]>, Shape.clash(accepted))
    case 3n <> 1n <> 1n <> (4n+p) <> Nil{}:
      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)))))
    case 3n <> 1n <> 2n <> 0n <> Nil{}:
      Certified{{==}, {==}, {==}, A => items => length => lists_3120(A, items, length),
        dims => length => product_3120(dims, length), dims => coords => dl => cl => fit_3120(dims, coords, dl, cl)}
    case 3n <> 1n <> 2n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 1n, 2n, 1n]>, Shape.clash(accepted))
    case 3n <> 1n <> 2n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 1n, 2n, 2n]>, Shape.clash(accepted))
    case 3n <> 1n <> 2n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 1n, 2n, 3n]>, Shape.clash(accepted))
    case 3n <> 1n <> 2n <> (4n+p) <> Nil{}:
      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)))))
    case 3n <> 1n <> 3n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 1n, 3n, 0n]>, Shape.clash(accepted))
    case 3n <> 1n <> 3n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 1n, 3n, 1n]>, Shape.clash(accepted))
    case 3n <> 1n <> 3n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 1n, 3n, 2n]>, Shape.clash(accepted))
    case 3n <> 1n <> 3n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 1n, 3n, 3n]>, Shape.clash(accepted))
    case 3n <> 1n <> 3n <> (4n+p) <> Nil{}:
      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)))))
    case 3n <> 1n <> (4n+p) <> a0 <> Nil{}:
      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)))))
    case 3n <> 2n <> 0n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 2n, 0n, 0n]>, Shape.clash(accepted))
    case 3n <> 2n <> 0n <> 1n <> Nil{}:
      Certified{{==}, {==}, {==}, A => items => length => lists_3201(A, items, length),
        dims => length => product_3201(dims, length), dims => coords => dl => cl => fit_3201(dims, coords, dl, cl)}
    case 3n <> 2n <> 0n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 2n, 0n, 2n]>, Shape.clash(accepted))
    case 3n <> 2n <> 0n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 2n, 0n, 3n]>, Shape.clash(accepted))
    case 3n <> 2n <> 0n <> (4n+p) <> Nil{}:
      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)))))
    case 3n <> 2n <> 1n <> 0n <> Nil{}:
      Certified{{==}, {==}, {==}, A => items => length => lists_3210(A, items, length),
        dims => length => product_3210(dims, length), dims => coords => dl => cl => fit_3210(dims, coords, dl, cl)}
    case 3n <> 2n <> 1n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 2n, 1n, 1n]>, Shape.clash(accepted))
    case 3n <> 2n <> 1n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 2n, 1n, 2n]>, Shape.clash(accepted))
    case 3n <> 2n <> 1n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 2n, 1n, 3n]>, Shape.clash(accepted))
    case 3n <> 2n <> 1n <> (4n+p) <> Nil{}:
      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)))))
    case 3n <> 2n <> 2n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 2n, 2n, 0n]>, Shape.clash(accepted))
    case 3n <> 2n <> 2n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 2n, 2n, 1n]>, Shape.clash(accepted))
    case 3n <> 2n <> 2n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 2n, 2n, 2n]>, Shape.clash(accepted))
    case 3n <> 2n <> 2n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 2n, 2n, 3n]>, Shape.clash(accepted))
    case 3n <> 2n <> 2n <> (4n+p) <> Nil{}:
      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)))))
    case 3n <> 2n <> 3n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 2n, 3n, 0n]>, Shape.clash(accepted))
    case 3n <> 2n <> 3n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 2n, 3n, 1n]>, Shape.clash(accepted))
    case 3n <> 2n <> 3n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 2n, 3n, 2n]>, Shape.clash(accepted))
    case 3n <> 2n <> 3n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 2n, 3n, 3n]>, Shape.clash(accepted))
    case 3n <> 2n <> 3n <> (4n+p) <> Nil{}:
      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)))))
    case 3n <> 2n <> (4n+p) <> a0 <> Nil{}:
      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)))))
    case 3n <> 3n <> 0n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 3n, 0n, 0n]>, Shape.clash(accepted))
    case 3n <> 3n <> 0n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 3n, 0n, 1n]>, Shape.clash(accepted))
    case 3n <> 3n <> 0n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 3n, 0n, 2n]>, Shape.clash(accepted))
    case 3n <> 3n <> 0n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 3n, 0n, 3n]>, Shape.clash(accepted))
    case 3n <> 3n <> 0n <> (4n+p) <> Nil{}:
      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)))))
    case 3n <> 3n <> 1n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 3n, 1n, 0n]>, Shape.clash(accepted))
    case 3n <> 3n <> 1n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 3n, 1n, 1n]>, Shape.clash(accepted))
    case 3n <> 3n <> 1n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 3n, 1n, 2n]>, Shape.clash(accepted))
    case 3n <> 3n <> 1n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 3n, 1n, 3n]>, Shape.clash(accepted))
    case 3n <> 3n <> 1n <> (4n+p) <> Nil{}:
      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)))))
    case 3n <> 3n <> 2n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 3n, 2n, 0n]>, Shape.clash(accepted))
    case 3n <> 3n <> 2n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 3n, 2n, 1n]>, Shape.clash(accepted))
    case 3n <> 3n <> 2n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 3n, 2n, 2n]>, Shape.clash(accepted))
    case 3n <> 3n <> 2n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 3n, 2n, 3n]>, Shape.clash(accepted))
    case 3n <> 3n <> 2n <> (4n+p) <> Nil{}:
      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)))))
    case 3n <> 3n <> 3n <> 0n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 3n, 3n, 0n]>, Shape.clash(accepted))
    case 3n <> 3n <> 3n <> 1n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 3n, 3n, 1n]>, Shape.clash(accepted))
    case 3n <> 3n <> 3n <> 2n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 3n, 3n, 2n]>, Shape.clash(accepted))
    case 3n <> 3n <> 3n <> 3n <> Nil{}:
      Empty.absurd(Facts<4n, [3n, 3n, 3n, 3n]>, Shape.clash(accepted))
    case 3n <> 3n <> 3n <> (4n+p) <> Nil{}:
      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)))))
    case 3n <> 3n <> (4n+p) <> a0 <> Nil{}:
      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)))))
    case 3n <> (4n+p) <> a0 <> a1 <> Nil{}:
      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)))))
    case (4n+p) <> a0 <> a1 <> a2 <> Nil{}:
      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)))))
    case +a0 <> +a1 <> +a2 <> +a3 <> +a4 <> +tail:
      Empty.absurd(Facts<4n, a0 <> a1 <> a2 <> a3 <> a4 <> tail>, Shape.clash(accepted))

Uses (85):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=clash
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=and_left
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=lt_zero
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=Facts
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=fit_0123
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=fit_0132
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=fit_0213
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=fit_0231
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=fit_0312
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=fit_0321
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=fit_1023
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=fit_1032
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=fit_1203
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=fit_1230
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=fit_1302
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=fit_1320
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=fit_2013
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=fit_2031
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=fit_2103
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=fit_2130
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=fit_2301
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=fit_2310
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=fit_3012
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=fit_3021
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=fit_3102
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=fit_3120
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=fit_3201
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=fit_3210
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=lists_0123
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=lists_0132
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=lists_0213
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=lists_0231
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=lists_0312
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=lists_0321
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=lists_1023
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=lists_1032
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=lists_1203
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=lists_1230
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=lists_1302
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=lists_1320
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=lists_2013
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=lists_2031
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=lists_2103
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=lists_2130
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=lists_2301
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=lists_2310
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=lists_3012
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=lists_3021
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=lists_3102
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=lists_3120
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=lists_3201
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=lists_3210
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=product_0123
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=product_0132
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=product_0213
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=product_0231
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=product_0312
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=product_0321
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=product_1023
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=product_1032
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=product_1203
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=product_1230
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=product_1302
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=product_1320
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=product_2013
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=product_2031
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=product_2103
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=product_2130
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=product_2301
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=product_2310
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=product_3012
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=product_3021
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=product_3102
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=product_3120
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=product_3201
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=product_3210
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_spec.bend&name=bounded
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_spec.bend&name=unique
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_spec.bend&name=valid