fact: Fixpoint cl_term (t : term) : cls -> class := fun i : cls => match t with | Srt _ => Knd PROP | Ref n => match Tnth_def _ Trm i n with | Knd s => Typ s | _ => Trm end | Abs A B => let j := TCs _ (cl_term A i) i in match cl_term B j, cl_term A i with | Typ s2, Knd s1 => Typ (PROD s1 s2) | Typ s, _ => Typ s | Knd _, _ => Knd PROP | Trm, _ => Trm end | App u v => match cl_term u i, cl_term v i with | Typ (PROD s1 s2), Typ s => Typ s2 | Typ s, _ => Typ s | Knd _, _ => Knd PROP | Trm, _ => Trm end | Prod T U => let j := TCs _ (cl_term T i) i in match cl_term U j, cl_term T i with | Knd s2, Knd s1 => Knd (PROD s1 s2) | Knd s, _ => Knd s | Typ s, _ => Typ s | c1, _ => c1 end end.
imports: Termes Conv Types ListType