CookLevin.polyTime_dropLast_append_child_reduction_child

import Definitions.Def_CookLevin_Basic
import Definitions.Def_CookLevin_Satisfiability
import Definitions.Def_CookLevin_Complexity
import Definitions.Def_CookLevin_Reduction

open CookLevin

theorem CookLevin.polyTime_dropLast_append_child_reduction_child
    (u v : List Bool → List Bool)
    (hu : IsPolyTimeComputable u)
    (hv : IsPolyTimeComputable v) :
    IsPolyTimeComputable (fun x => (u x).dropLast ++ v x) := by sorry