proposition: Lemma list_sim_length : forall l l', list_sim l l' -> length l = length l'.
proof: Proof. induction l; intros. inversion H; trivial. destruct l'. inversion H. simpl. rewrite (IHl l'); trivial. inversion H; trivial. Qed.
imports: Coq(Setoid Morphisms Basics) CoLoR(ListExtras NatUtil LogicUtil)