DEFINITION getl_gen_2()
TYPE =
       ∀c1:C.∀c2:C.∀i:nat.(getl i c1 c2)→(ex_3 B C T λb:B.λc:C.λv:T.eq C c2 (CHead c (Bind b) v))
BODY =
Show proof