proposition: Lemma In2_rev : forall i j l, In2 i j (rev l) <-> In2 j i l.
proof: Proof. intros i j l; unfold rev; rewrite In2_rev_aux; split; auto with smtcoq_in2; intros [H|[[_ H]|H]]; auto with smtcoq_in2; inversion H. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz