proposition: Lemma cast_eqb A B k: cast A B = Cast k -> eqb A B = true.
proof: Proof. intros. apply not_false_iff_true. unfold not. intro. apply cast_diff in H0. rewrite H in H0. inversion H0. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList