(n: nat).(csuba_refl g (CSort n))) (\lambda (c3: C).(\lambda (c4: C).(\lambda
(_: (csubc g c3 c4)).(\lambda (H1: (csuba g c3 c4)).(\lambda (k: K).(\lambda
(v: T).(csuba_head g c3 c4 H1 k v))))))) (\lambda (c3: C).(\lambda (c4:
(n: nat).(csuba_refl g (CSort n))) (\lambda (c3: C).(\lambda (c4: C).(\lambda
(_: (csubc g c3 c4)).(\lambda (H1: (csuba g c3 c4)).(\lambda (k: K).(\lambda
(v: T).(csuba_head g c3 c4 H1 k v))))))) (\lambda (c3: C).(\lambda (c4: