fact: Fixpoint active_position t p {struct p} : bool := match p with | nil => true | i :: q => match t with | Var _ => false | Term f l => andb (mem_bool Nat.eqb i (mu f)) (match nth_error l i with | None => false | Some ti => active_position ti q end) end end.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure decidable_set more_list weaved_relation term_spec equational_theory_spec dp rpo)