proposition: Lemma list_sim_tail : forall l l', list_sim l l' -> list_sim (tail l) (tail l').
proof: Proof. intros. destruct H; trivial. simpl; constructor. Qed.
imports: Coq(Setoid Morphisms Basics) CoLoR(ListExtras NatUtil LogicUtil)