125
125
thick-injective {suc n} (suc i) zero zero _ = refl
126
126
thick-injective {suc n} (suc i) zero (suc k) ()
127
127
thick-injective {suc n} (suc i) (suc j) zero ()
131
131
------------------------------------------------------------------------
132
132
-- The countdown data structure