- "belongs to complete (preterm)"
- 'UpDownArrowEpsilon p t = (preterm_in_comp p t).
-
-definition preterm_in_root: relation2 path preterm ≝
- λp,t. ∃q. p;;q ϵ⬦ t.
-
-interpretation
- "belongs to root (preterm)"
- 'UpArrowEpsilon p t = (preterm_in_root p t).