{Γ : Type u} →
  {Γ' : Type v} →
    [inst : Inhabited Γ] →
      [inst_1 : Inhabited Γ'] →
        {motive : Turing.PointedMap Γ Γ' → Sort u_1} →
          (t : Turing.PointedMap Γ Γ') →
            ((f : Γ → Γ') → (map_pt' : f default = default) → motive { f := f, map_pt' := map_pt' }) → motive t