-definition tm_ap (V) (T) ≝ ⓐV.T.
-
-definition tm_vlift (j) (gv): tm_evaluation ≝ λi. ↑[j,1](gv i).
-
-interpretation "lift (term model evaluation)"
- 'DottedUpArrow i gv = (tm_vlift i gv).
-
-definition tm_vpush (j) (T) (lv): tm_evaluation ≝
- λi. tri … i j (lv i) T (↑[j,1](lv (↓i))).
-
-interpretation "push (term model evaluation)"
- 'DottedUpArrow i d lv = (tm_vpush i d lv).