>>800
絶対にnullにならない証明付きのxsしか受け取らないっていう保障
head_tailを使う為にxsがnullになら無い証明を使用者に強制できる
逆にこの戻り値はこの関数を使用したときに別の関数で利用できる証明を含んでるから
この証明を使って別の関数が要求する証明を組み立てることに使ったりする