proposition: Lemma neq_cast : forall A B, cast A B = (if eqb A B then cast A B else NoCast).
proof: Proof. intros C D;case_eq (eqb C D);trivial;apply cast_diff. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList