reflexivity using (.≅.)
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✝¹
no goals