proposition: Theorem jump_add: forall a b l, jump (a + b) l = jump b (jump a l).
proof: Proof. intros a. induction a; auto; intros b l. - destruct l; simpl. + rewrite jump_nil. reflexivity. + apply IHa. Qed.
imports: List ListAux UList OrderedList