the launch covers the bank: its image walks exactly the bank's elements
2566def cgAdamWCoversTheBank : (equal Nat coppeliusAdamWElements cgParameterElements) =
2567 (refl Nat cgParameterElements)The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.