proposition: Lemma Psi_in_context_bis : forall f l k, (exists t, In t l /\ ~nf (one_step R) t) -> k = map psi l -> Psi (Term f k) (Term f l).
proof: Proof. intros f l k K H; subst k. replace (map psi l) with (map (@fst term term) (map (fun t => (psi t,t)) l)). replace (Term f l) with (Term f (map (@snd term term) (map (fun t => (psi t,t)) l))). apply Psi_in_context. intros s t st_in_ll; rewrite in_map_iff in st_in_ll. destruct st_in_ll as [t' [H t_in_l]]; injection H; clear H; intros; subst s t'. destruct (psi_char t) as [[H1 H2] | P]. right; split; trivial. left; trivial. destruct K as [t [t_in_l not_nf_t]]. exists (psi t); exists t; split; trivial. rewrite in_map_iff; exists t; split; trivial. apply (f_equal (fun l => Term f l)). pattern l at 2; rewrite <- map_id. rewrite map_map; apply map_eq; intros s _; simpl; trivial. rewrite map_map; apply map_eq; intros s _; simpl; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure more_list weaved_relation term equational_theory_spec rwr_strategies dp rpo)