proposition: Lemma recover_red : forall f l t s' t', defined R2 f -> Interp_dom R1 R2 (Term f l) -> Interp (Term f l) s' -> Interp t t' -> one_step (@union _ R1 R2) t (Term f l) -> rwr (Pi pi V0 V1) t' s'.
proof: Proof. intros f l t s' t' Df Idfl Is It t_R_fl. inversion Is as [ | f' l' l'' ll Cf Hl Hl' Hll | f' l' l'' ll _ Hl Hl' Hll]; subst. absurd (defined R2 f); trivial. apply project_comb. rewrite in_map_iff; exists (t,t'); split. apply eq_refl. assert (t_R_fl_bis := t_R_fl); rewrite FB12 in t_R_fl_bis. rewrite Hl in t_R_fl_bis. rewrite in_map_iff in t_R_fl_bis. destruct t_R_fl_bis as [[u u'] [u_eq_t H]]. simpl in u_eq_t; subst u. replace t' with u'; trivial. apply interp_unicity with t; trivial. apply interp_well_defined_2 with f l; trivial. apply Hll; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)