proposition: Lemma is_a_cycle_discard : forall c x x_val sigma src current, ~In x (current :: c) -> is_a_cycle sigma src current c = is_a_cycle ((x,x_val) :: sigma) src current c.
proof: Proof. intro c; induction c as [ | next c]; intros x x_val sigma src current W; simpl. generalize (X.eq_bool_ok current x); case (X.eq_bool current x); [intro current_eq_x | intros _; trivial]. apply False_rect; apply W; left; assumption. rewrite (IHc x x_val). generalize (X.eq_bool_ok current x); case (X.eq_bool current x); [intro current_eq_x | intros _; trivial]. apply False_rect; apply W; left; assumption. intro x_in_next_c; apply W; right; trivial. Qed.
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)