proposition: Lemma check_distinct_two_args_spec : forall f1 f2, check_distinct_two_args f1 f2 = true <-> exists ha hb ty x y, get_form f1 = Fatom ha /\ get_form f2 = Fatom hb /\ get_atom ha = Atom.Anop (Atom.NO_distinct ty) (x::y::nil) /\ (get_atom hb = Atom.Abop (Atom.BO_eq ty) x y \/ get_atom hb = Atom.Abop (Atom.BO_eq ty) y x).
proof: Proof. intros f1 f2; unfold check_distinct_two_args; split. case (get_form f1); try discriminate; intro ha; case (get_form f2); try discriminate; intro hb; case_eq (get_atom ha); try discriminate; intros [A] [ |x [ |y [ |l]]] Heq1; try discriminate; case_eq (get_atom hb); try discriminate; intros [ | | | | | | |B | | | | | | | | | | | | ] x' y' Heq2; try discriminate; rewrite !andb_true_iff, orb_true_iff, !andb_true_iff; change (Typ.eqb A B = true) with (is_true (Typ.eqb A B)); rewrite Typ.eqb_spec, !Int63.eqb_spec; intros [H1 [[H2 H3]|[H2 H3]]]; subst B x' y'; exists ha, hb, A, x, y; auto. intros [ha [hb [A [x [y [H1 [H2 [H3 [H4|H4]]]]]]]]]; rewrite H1, H2, H3, H4, Typ.eqb_refl, !eqb_refl; auto; rewrite orb_true_r; auto. Qed.
imports: List PArray Bool Int63 ZMicromega Misc State SMT_terms