proposition: Lemma iter_int63_comm : forall i A f a, iter_int63 i A f (f a) = f (iter_int63 i A f a).
proof: Proof. intros i A f a. unfold iter_int63. apply iter_int63_aux_comm. apply pow2_size. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz