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