rw [HList.cons_append]
case cons
αs : List (Sort u_1)
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : a✝.append nil ≅ a✝
⊢ (a✝¹ :: a✝).append nil ≅ a✝¹ :: a✝
case cons
αs : List (Sort u_1)
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : a✝.append nil ≅ a✝
⊢ a✝¹ :: a✝.append nil ≅ a✝¹ :: a✝