proposition: Lemma check_args_dec : forall tr args targs, {exists T : Typ.type, check_args args targs && Typ.eqb tr T} + {forall T : Typ.type, check_args args targs && Typ.eqb tr T = false}.
proof: Proof. intro A; induction args as [ |h l IHl]; simpl. intros [ | ]; simpl. left; exists A; apply Typ.eqb_refl. intros; right; reflexivity. intros [ |B targs]; simpl. right; reflexivity. case (Typ.eqb (get_type h) B); simpl; auto. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList