proposition: Lemma Bval_inj2 : forall T t u, Bval T t = Bval T u -> t = u.
proof: Proof. intros T t u H; assert (H1: (fun (x:bval) => match Typ.cast (v_type _ _ x) T with | Typ.Cast k => k _ (v_val _ _ x) = v_val _ _ (Bval T u) | Typ.NoCast => True end) (Bval T t)). rewrite H, Typ.cast_refl; reflexivity. simpl in H1; rewrite Typ.cast_refl in H1; auto. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList