proposition: Lemma In2_rev_aux : forall i j l acc, In2 i j (rev_aux acc l) <-> In2 i j acc \/ (In i l /\ In j acc) \/ In2 j i l.
proof: Proof. intros i j; induction l as [ |t q IHq]; simpl; intro acc; split; auto with smtcoq_in2. intros [H|[[H _]|H]]; auto with smtcoq_in2. elim H. inversion H. rewrite IHq; clear IHq; intros [H|[[H1 H2]|H]]; auto with smtcoq_in2. inversion H; auto with smtcoq_in2. inversion H2; auto with smtcoq_in2; clear H2; subst t; right; right; auto with smtcoq_in2. intros [H|[[[H1|H1] H2]|H]]; rewrite IHq; clear IHq; auto with smtcoq_in2. subst t; auto with smtcoq_in2. right; left; split; auto with smtcoq_in2; constructor 2; auto with smtcoq_in2. inversion H; clear H; auto with smtcoq_in2; subst j l; right; left; split; auto with smtcoq_in2; constructor 1; auto with smtcoq_in2. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz