∀[T:Type]. ∀[L:T List].  (hd(rev(L)) ~ last(L))
{ (UnivCD THENA Auto) }
1. T : Type
2. L : T List
⊢ hd(rev(L)) ~ last(L)