proposition: Lemma almost_const : forall f l, (forall t, In t l -> Acc (one_step R) t) -> (match F.arity f with Free n => n | _ => 2 end ) <> length l -> Acc (one_step R) (Term f l).
proof: Proof. intros f l Acc_l; revert f. rewrite acc_one_step_list in Acc_l; induction Acc_l as [l Acc_l IHl]. intros f L; apply Acc_intro. intros s H; inversion H as [t1 t2 H1 | g l1 l2 H2]; clear H; subst. inversion H1 as [r l' sigma H2]. destruct l' as [ | g l']. apply False_rect; apply (R_var _ _ H2). apply False_rect; apply L; injection H0; clear H0; intros; subst. rewrite map_length. assert (Wf := WR _ _ H2). destruct (well_formed_unfold (proj2 Wf)) as [_ L']. apply sym_eq; destruct (F.arity f); trivial. apply IHl; trivial. replace (length l1) with (length l); trivial. apply sym_eq; apply rwr_list_length_eq with (one_step R). left; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)