fact: Fixpoint is_a_cycle sigma src current c : bool := match c with | nil => match find X.eq_bool current sigma with | None => false | Some (Var x) => false | Some current_val => var_in_term src current_val end | next :: c' => match find X.eq_bool current sigma with | None => false | Some (Var x) => false | Some current_val => if var_in_term next current_val then is_a_cycle sigma src next c' else false end end.
imports: Coq(Arith Wf_nat Wellfounded List Multiset Relations) CoLoR(closure decidable_set ordered_set more_list list_permut list_set list_sort dickson term_spec term)