fact: Fixpoint termAtPos M (pos: Pos M) : Term := match pos with | PThis M => M | PAbs pos => termAtPos pos | PAppL _ pos => termAtPos pos | PAppR _ pos => termAtPos pos end.
imports: CoLoR(RelExtras ListExtras TermsBuilding)