proposition: Lemma Acc_Rwf : (forall s, well_formed s -> Acc (one_step R) s) -> forall s, well_formed s -> Acc Rwf s.
proof: Proof. intros W s Ws. apply Acc_incl with (fun x0 y : T1.term => one_step R (collapse_subst x0) (collapse_subst y)). intros t1 t2 H; inversion H; trivial. apply (Wellfounded.Inverse_Image.Acc_inverse_image term term (one_step R) collapse_subst). apply W; unfold collapse_subst; apply well_formed_apply_subst; trivial. unfold well_formed_subst. intros v; case_eq (find X.eq_bool v (map (fun v0 => (v0, T1.Var (inject 0))) (T1.var_list s))); [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. reflexivity. trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)