proposition: Theorem olist_weight: forall a b l, olist (a :: l) -> In b l -> weight a b = lt.
proof: Proof. intros a b l H; generalize a b H; elim l; clear a b l H. intros a b _ H1; case H1. simpl; intros a1 l Rec a b H [H1 | H1]; subst; auto. inversion H; auto. assert (Eq1: weight a a1 = lt). inversion H; auto. rewrite weight_trans with (b := a1); auto. rewrite Eq1; apply sym_equal; apply Rec; auto. inversion_clear H; auto. Qed.
imports: List Permutation UList