proposition: Lemma onlist_withdraw : forall (T:Type) (u:list T) (f:list T -> T), (onlist (u:=u) (withdraw (length u) f)) = f u.
proof: Proof. intros T u. induction u. intro f; reflexivity. intro f. transitivity (onlist (u:=u) ((withdraw (S (length u)) f) t)). reflexivity. exact (IHu (fun u => f (cons t u))). Qed.