fact: Fixpoint check_args (args:list hatom) (targs:list Typ.type) := match args, targs with | nil, nil => true | a::args, t::targs => Typ.eqb (get_type a) t && check_args args targs | _, _ => false end.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList