fact: Definition check_distinct_two_args f1 f2 := match get_form f1, get_form f2 with | Fatom ha, Fatom hb => match get_atom ha, get_atom hb with | Atom.Anop (Atom.NO_distinct ty) (x::y::nil), Atom.Abop (Atom.BO_eq ty') x' y' => (Typ.eqb ty ty') && (((x =? x') && (y =? y')) || ((x =? y') && (y =? x'))) | _, _ => false end | _, _ => false end.
imports: List PArray Bool Int63 ZMicromega Misc State SMT_terms