proposition: Lemma get_eq_interp : forall (l:_lit) (f:Atom.hatom -> Atom.hatom -> C.t), (forall xa, t_form.[Lit.blit l] = Form.Fatom xa -> forall t a b, t_atom.[xa] = Atom.Abop (Atom.BO_eq t) a b -> rho (Lit.blit l) = Atom.interp_bool t_i (Atom.apply_binop t_i t t Typ.Tbool (Typ.i_eqb t_i t) (interp_hatom a) (interp_hatom b)) -> Typ.eqb (get_type a) t -> Typ.eqb (get_type b) t -> C.interp rho (f a b)) -> C.interp rho (get_eq (Lit.blit l) f).
proof: Proof. intros l f Hf;unfold get_eq. case_eq (t_form.[Lit.blit l]);trivial with smtcoq_euf;intros. case_eq (t_atom.[i]);trivial with smtcoq_euf;intros. destruct b;trivial with smtcoq_euf. generalize wt_t_atom;unfold Atom.wt;unfold is_true; rewrite Misc.aforallbi_spec;intros. assert (i <? length t_atom). apply PArray.get_not_default_lt. rewrite H0, def_t_atom;discriminate. apply H1 in H2;clear H1;rewrite H0 in H2;simpl in H2. rewrite !andb_true_iff in H2;decompose [and] H2;clear H2. apply Hf with (2:= H0);trivial. rewrite wf_interp_form, H;simpl. unfold Atom.interp_form_hatom, Atom.interp_hatom at 1;simpl. rewrite Atom.t_interp_wf, H0;simpl;trivial. Qed.
imports: Bool List Int63 PArray State SMT_terms