- "grafted (preterm)"
- 'Pitchfork t p = (preterm_grafted p t).
-
-definition preterm_root: preterm → preterm ≝
- λt,q. ∃r. q●r ϵ t.
-
-interpretation
- "root (preterm)"
- 'UpTriangle t = (preterm_root t).
-
-(* Basic constructions ******************************************************)
-
-lemma preterm_in_comp_root (p) (t):
- p ϵ t → p ϵ ▵t.
-/2 width=2 by ex_intro/
-qed.