proposition: Lemma check_aux_interp_aux : forall a t, check_aux get_type a t -> exists v, interp_aux (get t_interp) a = (Bval t v).
proof: Proof. intros a t; apply check_aux_interp_aux_aux; apply check_aux_interp_hatom. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList