apply HList.cons_hcongr
case cons
αs βs γs : List (Sort u_1)
bs : HList βs
cs : HList γs
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : (a✝.append bs).append cs ≅ a✝.append (bs.append cs)
⊢ a✝¹ :: (a✝.append bs).append cs ≅ (a✝¹ :: a✝).append (bs.append cs)
case cons.a
αs βs γs : List (Sort u_1)
bs : HList βs
cs : HList γs
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : (a✝.append bs).append cs ≅ a✝.append (bs.append cs)
⊢ α✝ = α✝

case cons.a
αs βs γs : List (Sort u_1)
bs : HList βs
cs : HList γs
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : (a✝.append bs).append cs ≅ a✝.append (bs.append cs)
⊢ αs✝ ++ βs ++ γs = αs✝ ++ (βs ++ γs)

case cons.a
αs βs γs : List (Sort u_1)
bs : HList βs
cs : HList γs
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : (a✝.append bs).append cs ≅ a✝.append (bs.append cs)
⊢ a✝¹ ≅ a✝¹

case cons.a
αs βs γs : List (Sort u_1)
bs : HList βs
cs : HList γs
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : (a✝.append bs).append cs ≅ a✝.append (bs.append cs)
⊢ (a✝.append bs).append cs ≅ a✝.append (bs.append cs)