proposition: Lemma check_args_interp_aux_contr : forall l f, (forall T : Typ.type, (let (targs, tr) := v_type Typ.ftype interp_ft f in check_args get_type l targs && Typ.eqb tr T) = false) -> (let (tf, f0) := f in apply_func (fst tf) (snd tf) f0 (List.map interp_hatom l)) = bvtrue.
proof: Proof. induction l as [ |h l IHl]; simpl; intros [tf f]; simpl. destruct tf as [[ | ] tr]; simpl; auto; intro H; generalize (H tr); rewrite Typ.eqb_refl; discriminate. destruct tf as [[ |B targs] tr]; simpl; auto. intro H. destruct (check_aux_interp_hatom h) as [v Hv]. rewrite Hv. simpl. assert (H2: (Typ.eqb (get_type h) B = false) \/ (forall T : Typ.type, check_args get_type l targs && Typ.eqb tr T = false)) by (case_eq (Typ.eqb (get_type h) B); try (intros; left; reflexivity); intro Heq; right; intro T; generalize (H T); rewrite Heq; auto). destruct H2 as [H2|H2]; rewrite Typ.neq_cast. rewrite H2. auto. case_eq (Typ.eqb (get_type h) B); auto. change (Typ.eqb (get_type h) B = true) with (is_true (Typ.eqb (get_type h) B)). rewrite Typ.eqb_spec. intro; subst B. rewrite Typ.cast_refl. apply (IHl (Tval (targs,tr) (f v))). auto. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList