fact: Definition wt t_atom := let t_interp := t_interp t_atom in let get_type := get_type' t_interp in aforallbi (fun i h => check_aux get_type h (get_type i)) t_atom.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList