fact: Fixpoint int_term (t : term) : intt -> nat -> term := fun (I : intt) (k : nat) => match t with | Srt s => Srt s | Ref n => match le_gt_dec k n with | left _ => lift k (I (n - k)) | right _ => Ref n end | Abs A t => Abs (int_term A I k) (int_term t I (S k)) | App u v => App (int_term u I k) (int_term v I k) | Prod A B => Prod (int_term A I k) (int_term B I (S k)) end.
imports: Termes