fact: Definition check_diseq l : C.t := match get_form (Lit.blit l) with |Form.For a => if PArray.length a =? 3 then let a_eq_b := a.[0] in let not_a_le_b := a.[1] in let not_b_le_a := a.[2] in get_eq a_eq_b (fun a b => get_not_le not_a_le_b (fun a' b' => get_not_le not_b_le_a (fun b'' a'' => if (a =? a') && (a =? a'') && (b =? b') && (b =? b'') then (Lit.lit (Lit.blit l))::nil else if (a =? b') && (a =? b'') && (b =? a') && (b =? a'') then (Lit.lit (Lit.blit l))::nil else C._true))) else C._true | _ => C._true end.
imports: Bool List Int63 Ring63 PArray ZArith Misc State SMT_terms Euf RingMicromega ZMicromega Coq.micromega.Tauto Psatz