fact: Fixpoint int_typ (T : term) : intP -> forall s : skel, Can s := fun (ip : intP) (s : skel) => match T with | Srt _ => default_can s | Ref n => coerce_CR s (Tnth_def _ (iK PROP sn) ip n) | Abs A t => match cl_term A (cls_of_int ip) with | Knd _ => match s as x return (Can x) with | PROD s1 s2 => fun C : Can s1 => int_typ t (TCs _ (iK s1 C) ip) s2 | PROP => default_can PROP end | Typ _ => int_typ t (def_cons A ip) s | _ => default_can s end | App u v => match cl_term v (cls_of_int ip) with | Trm => int_typ u ip s | Typ sv => int_typ u ip (PROD sv s) (int_typ v ip sv) | _ => default_can s end | Prod A B => match s as x return (Can x) with | PROP => let s := cv_skel (cl_term A (cls_of_int ip)) in Pi s (int_typ A ip PROP) (fun C => int_typ B (int_cons A ip s C) PROP) | PROD s1 s2 => default_can (PROD s1 s2) end end.
imports: Termes Conv Types Class Can