proposition: Lemma find_col : forall vars v, In v vars -> find X.eq_bool v (map (fun v0 : T1.variable => (v0, T1.Var (inject 0))) vars) = Some (Var (inject 0)).
proof: Proof. intros vars v v_in_vars. case_eq (find X.eq_bool v (map (fun v0 => (v0, T1.Var (inject 0))) vars)); [intros v_val v_col | intro v_col]. destruct (find_mem _ _ X.eq_bool_ok _ _ v_col) as [v' [col1 [col2 [v_eq_v' H]]]]; subst v'. assert (v_in_col : In (v,v_val) (col1 ++ (v,v_val) :: col2)). apply in_or_app; right; left; reflexivity. rewrite <- H in v_in_col; rewrite in_map_iff in v_in_col. destruct v_in_col as [v' [v_eq_v' v_in_col]]; injection v_eq_v'; intros; subst; simpl; trivial. apply False_rect; apply (find_not_found X.eq_bool v v (Var (inject 0)) _ v_col (eq_var_bool_refl v)). rewrite in_map_iff; exists v; split; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)