# Failures and slowdowns compared to intuition

While trying to port a bunch of code to use itauto instead of intuition, we found these strange failures and a slowdown. I did some workarounds for now, but would be grateful for an analysis if these are fundamental limitations or could be fixed in the future.

```
Require Import Cdcl.Itauto.
Require Import List.
Goal forall A (s1 s2 s : list A),
(forall x : A, In x s1 \/ In x s2 -> In x s) <->
(forall x : A, In x s1 -> In x s) /\ (forall x : A, In x s2 -> In x s).
Proof.
Fail itauto auto.
intuition auto.
Qed.
Goal forall A B (f : A -> option B) (l : list B) v0,
f v0 = None \/ (forall m : B, f v0 = Some m -> In m l) ->
forall m : B, f v0 = Some m -> In m l.
Proof.
Fail itauto congruence.
intuition congruence.
Qed.
Goal forall A a a0 (r l l' : list A), (In a l' <-> In a l /\ ~ In a r) ->
~ (~ In a0 r) ->
In a l' <-> (a = a0 \/ In a l) /\ ~ In a r.
Proof.
(* Loops: itauto auto. *)
(* Slow: Time itauto congruence. *)
Time split; itauto congruence.
Qed.
```