
        assert_eq!(
            Var(0).whnf(Subst::comp(
                Subst::comp(Subst::cons(Type::closure(Var(0), Id), Shift), Shift),
                Shift
            )),
            (Var(2), Id)
        );

        assert_eq!(
            Var(1).whnf(Subst::comp(
                Subst::cons(
                    Type::closure(Var(0), Id),