fact: Fixpoint is_a_pos (t : term) (p : list nat) {struct p}: bool := match p with | nil => true | i :: q => match t with | Var _ => false | Term _ l => match nth_error l i with | Some ti => is_a_pos ti q | None => false end end end.
imports: List more_list list_permut list_set Arith