(eqc ? (w24h w1) (w24h w2)) ⊗
(eqc ? (w24l w1) (w24l w2)).
+ndefinition succ_w24 ≝
+λw.match eqc ? (predc ? (zeroc ?)) (w24l w) with
+ [ true ⇒ match eqc ? (predc ? (zeroc ?)) (w24h w) with
+ [ true ⇒ 〈(succc ? (w24x w));(succc ? (w24h w));(succc ? (w24l w))〉
+ | false ⇒ 〈(w24x w);(succc ? (w24h w));(succc ? (w24l w))〉 ]
+ | false ⇒ 〈(w24x w);(w24h w);(succc ? (w24l w))〉 ].
+
nlemma word24_destruct_1 :
∀x1,x2,y1,y2,z1,z2.
mk_word24 x1 y1 z1 = mk_word24 x2 y2 z2 → x1 = x2.