proposition: Lemma check_aux_dec : forall a, {exists T, check_aux a T} + {forall T, check_aux a T = false}.
proof: Proof. intros [op|op h|op h1 h2|op ha i i0|f args | i e ]; simpl. left; destruct op; simpl. exists Typ.Tpositive; auto with smtcoq_core. exists Typ.TZ; auto with smtcoq_core. exists (Typ.TBV n); now rewrite N.eqb_refl. destruct op; simpl; (case (Typ.eqb (get_type h) Typ.Tpositive)). left; exists Typ.Tpositive; easy. right; intros; rewrite andb_false_r; easy. left; exists Typ.Tpositive; easy. right; intros; rewrite andb_false_r; easy. left; exists Typ.TZ; easy. right; intros; rewrite andb_false_r; easy. left; exists Typ.TZ; easy. right; intros; rewrite andb_false_r; easy. (case (Typ.eqb (get_type h) Typ.TZ)). left. exists Typ.TZ. easy. right. intros. rewrite andb_false_r. easy. (case (Typ.eqb (get_type h) Typ.TZ)). left. exists Typ.TZ. easy. right. intros. rewrite andb_false_r. easy. (case (Typ.eqb (get_type h) (Typ.TBV n))). left. exists Typ.Tbool. easy. right. intros. rewrite andb_false_r. easy. (case (Typ.eqb (get_type h) (Typ.TBV n))). left. exists Typ.Tbool. easy. right. intros. rewrite andb_false_r. easy. (case (Typ.eqb (get_type h) (Typ.TBV n))). left. exists (Typ.TBV n). now rewrite N.eqb_refl; easy. right. intros. rewrite andb_false_r. easy. (case (Typ.eqb (get_type h) (Typ.TBV n))). left. exists (Typ.TBV n). now rewrite N.eqb_refl; easy. right. intros. rewrite andb_false_r. easy. (case (Typ.eqb (get_type h) (Typ.TBV n))). left. exists (Typ.TBV n). now rewrite N.eqb_refl; easy. right. intros. rewrite andb_false_r. easy. (case (Typ.eqb (get_type h) (Typ.TBV n))). left. exists (Typ.TBV n). now rewrite N.eqb_refl; easy. right. intros. rewrite andb_false_r. easy. (case (Typ.eqb (get_type h) (Typ.TBV n1))). left. exists (Typ.TBV n0). now rewrite N.eqb_refl; easy. right. intros. rewrite andb_false_r. easy. (case (Typ.eqb (get_type h) (Typ.TBV n1))). left. exists (Typ.TBV n0). now rewrite N.eqb_refl; easy. right. intros. rewrite andb_false_r. easy. (case (Typ.eqb (get_type h) (Typ.TBV n))). left. exists (Typ.TBV (i + n)). now rewrite N.eqb_refl; easy. right. intros. rewrite andb_false_r. easy. (case (Typ.eqb (get_type h) (Typ.TBV n))). left. exists (Typ.TBV (i + n)). now rewrite N.eqb_refl; easy. right. intros. rewrite andb_false_r. easy. (case (Typ.eqb (get_type h) (Typ.TBV n))). left. exists (Typ.TBV (i + n)). now rewrite N.eqb_refl; easy. right. intros. rewrite andb_false_r. easy. (case (Typ.eqb (get_type h) (Typ.TBV n))). left. exists (Typ.TBV (i + n)). now rewrite N.eqb_refl; easy. right. intros. rewrite andb_false_r. easy. destruct op; simpl. (case (Typ.eqb (get_type h1) Typ.TZ)); (case (Typ.eqb (get_type h2) Typ.TZ)). left. exists Typ.TZ. easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. (case (Typ.eqb (get_type h1) Typ.TZ)); (case (Typ.eqb (get_type h2) Typ.TZ)). left. exists Typ.TZ. easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. (case (Typ.eqb (get_type h1) _)); (case (Typ.eqb (get_type h2) _ )). left. exists Typ.TZ. easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. (case (Typ.eqb (get_type h1) _)); (case (Typ.eqb (get_type h2) _)). left. exists Typ.Tbool. easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. (case (Typ.eqb (get_type h1) _)); (case (Typ.eqb (get_type h2) _)). left. exists Typ.Tbool. easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. (case (Typ.eqb (get_type h1) _)); (case (Typ.eqb (get_type h2) _)). left. exists Typ.Tbool. easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. (case (Typ.eqb (get_type h1) _)); (case (Typ.eqb (get_type h2) _)). left. exists Typ.Tbool. easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. (case (Typ.eqb (get_type h1) _)); (case (Typ.eqb (get_type h2) _)). left. exists Typ.Tbool. easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. (case (Typ.eqb (get_type h1) _)); (case (Typ.eqb (get_type h2) _)). left. exists (Typ.TBV n). now rewrite N.eqb_refl; easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. (case (Typ.eqb (get_type h1) _)); (case (Typ.eqb (get_type h2) _)). left. exists (Typ.TBV n). now rewrite N.eqb_refl; easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. (case (Typ.eqb (get_type h1) _)); (case (Typ.eqb (get_type h2) _)). left. exists (Typ.TBV n). now rewrite N.eqb_refl; easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. (case (Typ.eqb (get_type h1) _)); (case (Typ.eqb (get_type h2) _)). left. exists (Typ.TBV n). now rewrite N.eqb_refl; easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. (case (Typ.eqb (get_type h1) _)); (case (Typ.eqb (get_type h2) _)). left. exists (Typ.TBV n). now rewrite N.eqb_refl; easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. (case (Typ.eqb (get_type h1) _)); (case (Typ.eqb (get_type h2) _)). left. exists (Typ.Tbool). easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. (case (Typ.eqb (get_type h1) _)); (case (Typ.eqb (get_type h2) _)). left. exists (Typ.Tbool). easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. (case (Typ.eqb (get_type h1) _)); (case (Typ.eqb (get_type h2) _)). left. exists (Typ.TBV (n + n0)). rewrite N.eqb_refl. easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. (case (Typ.eqb (get_type h1) _)); (case (Typ.eqb (get_type h2) _)). left. exists (Typ.TBV n). now rewrite N.eqb_refl; easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. (case (Typ.eqb (get_type h1) _)); (case (Typ.eqb (get_type h2) _)). left. exists (Typ.TBV n). now rewrite N.eqb_refl; easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. (case (Typ.eqb (get_type h1) _)); (case (Typ.eqb (get_type h2) _)). left. exists t0. rewrite Typ.eqb_refl. easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. (case (Typ.eqb (get_type h1) _)); (case (Typ.eqb (get_type h2) _)). left. exists t. rewrite Typ.eqb_refl. easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. revert i i0; destruct op; simpl. intros h1 h2. (case (Typ.eqb (get_type h1) _)); (case (Typ.eqb (get_type h2) _)); (case (Typ.eqb (get_type ha) _)). left. exists (Typ.TFArray t t0). rewrite !Typ.eqb_refl. easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. right. intros. rewrite andb_false_r. easy. destruct f as [ty]; simpl; case (List.forallb (fun t1 : int => Typ.eqb (get_type t1) ty) args). left; exists Typ.Tbool; auto with smtcoq_core. right; intro T; rewrite andb_false_r; auto. case (v_type Typ.ftype interp_ft (t_func .[ i])); intros; apply check_args_dec. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList