proposition: Lemma is_a_cycle_all_var_inst : forall c sigma src current, is_a_cycle sigma src current c = true -> forall x, In x (current :: c) -> match find X.eq_bool x sigma with | Some (Term _ _) => True | _ => False end.
proof: Proof. simpl In; intros c sigma src current Hcycle x [x_eq_current | x_in_c]. subst x; destruct c; simpl in Hcycle. destruct (find X.eq_bool current sigma) as [[ | ] | ]; trivial; discriminate. destruct (find X.eq_bool current sigma) as [[ | ] | ]; trivial; discriminate. revert src current Hcycle; induction c as [ | next c]; intros src current Hcycle. contradiction. simpl in Hcycle. destruct (find X.eq_bool current sigma) as [[ v | f l] | ]; try discriminate. destruct (var_in_term next (Term f l)); [idtac | discriminate]. simpl in x_in_c; destruct x_in_c as [x_eq_next | x_in_c]. subst x; destruct c; simpl in Hcycle. destruct (find X.eq_bool next sigma) as [[v | g k] | ]; trivial; discriminate. destruct (find X.eq_bool next sigma) as [[v | g k] | ]; trivial; discriminate. apply (IHc x_in_c src next Hcycle). 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)