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