proposition: Lemma withdraw_onlist : forall (T:Type) (p:nat) (f : (forall m : nat, arity m T)), same_arity (withdraw p (fun u:list T => (onlist (u:=u) (f (length u))))) (f p).
proof: Proof. intros T p. induction p. intro f. set (g:= fun u : list T => onlist (u:=u) (f (length u))). change ((withdraw 0 g) = f 0). reflexivity. intro f. set (g:= fun u : list T => onlist (u:=u) (f (length u))). change (forall t:T, same_arity ((withdraw (S p) g) t) ((f (S p)) t)). intro t. exact (IHp (fun m => f (S m) t)). Qed.