proposition: Lemma find_map_subst : forall x y t sigma, match find X.eq_bool x sigma with | None => find X.eq_bool x (map_subst (fun (_ : variable) v_sigma => apply_subst ((y, t) :: nil) v_sigma) sigma) = None | Some x_val => find X.eq_bool x (map_subst (fun (_ : variable) v_sigma => apply_subst ((y, t) :: nil) v_sigma) sigma) = Some (apply_subst ((y, t) :: nil) x_val) end.
proof: Proof. intros x y s sigma; generalize x y s; clear x y s; induction sigma as [ | [z u] sigma]; intros x y s; simpl; trivial. generalize (X.eq_bool_ok x z); case (X.eq_bool x z); [intro x_eq_z; trivial | intro x_diff_z]. apply IHsigma. 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)