- (if_then_else T (eqb n k) (lift a n) (Rel (n-1)))
- | App m n ⇒ App (subst_aux m k a) (subst_aux n k a)
- | Lambda m n ⇒ Lambda (subst_aux m k a) (subst_aux n (k+1) a)
- | Prod m n ⇒ Prod (subst_aux m k a) (subst_aux n (k+1) a)
+ (if_then_else T (eqb n k) (lift a 0 n) (Rel (n-1)))
+ | App m n ⇒ App (subst m k a) (subst n k a)
+ | Lambda m n ⇒ Lambda (subst m k a) (subst n (k+1) a)
+ | Prod m n ⇒ Prod (subst m k a) (subst n (k+1) a)