proposition: Theorem type_of_correct : forall Gamma t T, type_of Gamma t = Some T -> has_type Gamma t T.
proof: Proof. intros. gen Gamma; gen T. induction t; intros; simpl 1 in *. - constructor; auto. - destruct (type_of Gamma t1) eqn: E. + simpl in H. rewrite E in H. simpl in H. destruct t; try discriminate. destruct (type_of Gamma t2) eqn: E'; try discriminate. simpl in *. destruct (type_eqb t3 t) eqn: E''; try discriminate. injection H as H. subst. apply type_eq_eqb in E''. subst. apply IHt2 in E'. apply IHt1 in E. econstructor; eauto. + simpl in H. rewrite E in *. discriminate. - simpl in *. unfold bindop in H. destruct (type_of (t_update Gamma s t) t0) eqn: E; try discriminate. injection H as H; subst. constructor. apply IHt. apply E. - injection H as H; subst. constructor. - injection H as H; subst; constructor. - simpl in H. destruct (type_of Gamma t1) eqn: E; destruct (type_of Gamma t2) eqn: E'; destruct (type_of Gamma t3) eqn: E''; simpl in H; try discriminate. apply IHt1 in E. apply IHt2 in E'. apply IHt3 in E''. destruct (type_eqb t <{ Bool }> && type_eqb t0 t4)%bool eqn: E'''; try discriminate. injection H as H; subst. apply Bool.andb_true_iff in E'''. destruct E'''. apply type_eq_eqb in H, H0. subst. constructor; auto. Qed.
imports: QuickChick(QuickChick) Coq(Nat) Coq(Arith.Arith) Coq(Logic.FunctionalExtensionality)