(Bind Abbr) u) (CHead c (Bind b) v))) (ex2 nat (\lambda (j: nat).(eq nat i (S
j))) (\lambda (j: nat).(getl j c (CHead d (Bind Abbr) u)))) (pr2 c (THead
(Bind b) v t3) (THead (Bind b) v t)) (\lambda (H7: (land (eq nat i O) (eq C
(Bind Abbr) u) (CHead c (Bind b) v))) (ex2 nat (\lambda (j: nat).(eq nat i (S
j))) (\lambda (j: nat).(getl j c (CHead d (Bind Abbr) u)))) (pr2 c (THead
(Bind b) v t3) (THead (Bind b) v t)) (\lambda (H7: (land (eq nat i O) (eq C