proposition: Theorem take_and_jump_nil: forall a b c, take_and_jump a b c nil = nil.
proof: Proof. intros a b c; elim c; simpl; auto. intros n H; rewrite jump_nil, take_nil, H; auto with arith. Qed.
imports: List ListAux UList OrderedList