fact: Fixpoint lift_rec n t {struct t} : nat -> term := fun k => match t with | Srt s => Srt s | Ref i => match le_gt_dec k i with | left _ => Ref (n + i) | right _ => Ref i end | Abs T M => Abs (lift_rec n T k) (lift_rec n M (S k)) | App u v => App (lift_rec n u k) (lift_rec n v k) | Prod A B => Prod (lift_rec n A k) (lift_rec n B (S k)) end.
imports: Arith Compare_dec Relations