fact: Fixpoint subst_rec N M {struct M} : nat -> term := fun k => match M with | Srt s => Srt s | Ref i => match lt_eq_lt_dec k i with | inleft C => match C with | left _ => Ref (pred i) | right _ => lift k N end | inright _ => Ref i end | Abs A B => Abs (subst_rec N A k) (subst_rec N B (S k)) | App u v => App (subst_rec N u k) (subst_rec N v k) | Prod T U => Prod (subst_rec N T k) (subst_rec N U (S k)) end.
imports: Arith Compare_dec Relations