proposition: Lemma list_sim_nth : forall p l l' a, list_sim l l' -> nth_error l p = Some a -> exists b, nth_error l' p = Some b /\ R a b.
proof: Proof. induction p. intros. inversion H. rewrite <- H1 in H0; discr. exists y; split; auto. replace a with x; trivial. rewrite <- H3 in H0; inversion H0; trivial. intros. destruct l; destruct l'; try discr. inversion H. inversion H. destruct (IHp l l' a); trivial. destruct H7. exists x0; split; trivial. Qed.
imports: Coq(Setoid Morphisms Basics) CoLoR(ListExtras NatUtil LogicUtil)