T).(pc3 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O))
(lift (S O) O t) x4)) H31 (TSort O) H35) in (let H39 \def (eq_ind C x10
(\lambda (c: C).(ty3 g c (TSort O) x12)) H37 (CHead (CSort O) (Bind Abst)
-(TSort O)) H36) in (and_ind (pc3 (CHead (CHead (CHead (CSort O) (Bind Abst)
+(TSort O)) H36) in (land_ind (pc3 (CHead (CHead (CHead (CSort O) (Bind Abst)
(TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S (S O)))
x0) (\forall (b: B).(\forall (u0: T).(pc3 (CHead (CHead (CHead (CHead (CSort
O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (Bind