apply HList.cons_hcongr
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.a
αs : List (Sort u_1)
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : a✝.append nil ≅ a✝
⊢ α✝ = α✝

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

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

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