proposition: Lemma check_aux_interp_aux_contr : forall a, (forall T, check_aux get_type a T = false) -> interp_aux (get t_interp) a = bvtrue.
proof: Proof. intros; eapply check_aux_interp_aux_contr_aux; eauto; apply check_aux_interp_hatom. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList