fact: Fixpoint check_distinct_elim input res := match input with | nil => nil | l::q => if check_lit' l res then res::q else l::(check_distinct_elim q res) end.
imports: List PArray Bool Int63 ZMicromega Misc State SMT_terms