(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
-(CHead d (Bind Abbr) u) (CHead c (Bind b) v)))).(and_ind (eq nat i O) (eq C
+(CHead d (Bind Abbr) u) (CHead c (Bind b) v)))).(land_ind (eq nat i O) (eq C
(CHead d (Bind Abbr) u) (CHead c (Bind b) v)) (pr2 c (THead (Bind b) v t3)
(THead (Bind b) v t)) (\lambda (H8: (eq nat i O)).(\lambda (H9: (eq C (CHead
d (Bind Abbr) u) (CHead c (Bind b) v))).(let H10 \def (f_equal C C (\lambda