fact: Definition c_in_context R shift f ls lt := exists n, C_list R n ls lt /\ In (shift + n) (mu f).
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure decidable_set more_list weaved_relation term_spec equational_theory_spec dp rpo)