proposition: Lemma nocast_refl A B: cast A B = NoCast -> cast B A = NoCast.
proof: Proof. intros. apply cast_diff. rewrite neq_cast in H. case_eq (eqb A B). intro. rewrite H0 in H. apply eqb_spec in H0. rewrite H0 in H. rewrite cast_refl in H. now contradict H. intro. apply not_true_iff_false. unfold not. intro. apply eqb_spec in H1. rewrite H1 in H0. rewrite eqb_refl in H0. now contradict H0. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList