proposition: Lemma unicity : forall a t1 t2, check_aux a t1 -> check_aux a t2 -> t1 = t2.
proof: Proof. destruct a;simpl. intros t1 t2;rewrite !Typ.eqb_spec;intros;subst;trivial. unfold is_true; intros t1 t2;rewrite (surjective_pairing (typ_uop u)),!andb_true_iff. intros [H1 _] [H2 _]; change (is_true (Typ.eqb (snd (typ_uop u)) t1)) in H1. change (is_true (Typ.eqb (snd (typ_uop u)) t2)) in H2. rewrite Typ.eqb_spec in H1, H2;subst;trivial. unfold is_true; intros t1 t2;rewrite (surjective_pairing (typ_bop b)), (surjective_pairing (fst (typ_bop b))) ,!andb_true_iff. intros [[H1 _] _] [[H2 _] _]; change (is_true (Typ.eqb (snd (typ_bop b)) t1)) in H1. change (is_true (Typ.eqb (snd (typ_bop b)) t2)) in H2. rewrite Typ.eqb_spec in H1, H2;subst;trivial. unfold is_true. intros. destruct typ_top. destruct p. destruct p. rewrite !andb_true_iff in H, H0. destruct H as (((Ha, Hb), Hc), Hd). destruct H0 as (((H0a, H0b), H0c), H0d). apply Typ.eqb_spec in Ha. apply Typ.eqb_spec in H0a. now subst. intros t1 t2; destruct (typ_nop n) as [ta t']; unfold is_true; rewrite !andb_true_iff; change (is_true (Typ.eqb t' t1) /\ is_true (List.forallb (fun t3 : int => Typ.eqb (get_type t3) ta) l) -> is_true (Typ.eqb t' t2) /\ is_true (List.forallb (fun t3 : int => Typ.eqb (get_type t3) ta) l) -> t1 = t2); rewrite !Typ.eqb_spec; intros [H1 _] [H2 _]; subst; auto. intros t1 t2;destruct (v_type Typ.ftype interp_ft (t_func.[ i])). unfold is_true;rewrite !andb_true_iff;intros [_ H1] [_ H2]. transitivity t;[ symmetry| ];rewrite <-Typ.eqb_spec;trivial. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList