fact: Variable P_ok : match v0 with | Var _ => True | Term f _ => match F.arity f with Free n => P f < n | _ => P f < 2 end end.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp) CoLoR(NatCompat)