proposition: Lemma i63_eqb_eq (x y : i63) : x =? y = true <-> x = y.
proof: Proof. destruct x as [x]. destruct y as [y]. cbv. split; intros equ. + apply eqb_correct in equ. now rewrite equ. + inversion equ; subst. apply eqb_refl. Qed.
imports: Coq(NArith ZArith Int63 Program.Wf)