proposition: Lemma expand_dp : forall dpR R t f l, rdp_step dpR R t (Term f l) <-> compose_rel dpR (refl_trans_clos (hide_in_context R)) t (Term f l).
proof: Proof. intros dpR R t f l; split. intro H; inversion H as [g l1 l2 H1 H2 H3]; subst. constructor 1 with (Term f l2); trivial. inversion H2 as [k | k1 k2 K2]; subst. left. right; clear -K2; induction K2 as [l1 l2 H | l1 l2 l3 H1 H2]. left; constructor; assumption. right with (Term f l2); [ constructor | ]; assumption. intro H; inversion H as [u1 u2 u3 H1 H2]; subst. assert (K : exists l2, u2 = Term f l2 /\ refl_trans_clos (one_step_list (one_step R)) l2 l). clear -H2; inversion H2 as [u | u1 v2 K2]; clear H2; subst. exists l; split; [apply eq_refl | left]. set (s := Term f l) in *. assert (s_eq_fl := eq_refl s). unfold s at 2 in s_eq_fl; clearbody s. revert f l s_eq_fl; induction K2 as [t1 t2 K | t1 t2 t3 K1 K2]; intros f l s_eq_fl. inversion K as [f' l1 l2]; clear K; subst. injection H1; clear H1; intros; subst f' l2. exists l1; split; [apply eq_refl | right; left; assumption]. inversion K1 as [f' l1 l2]; clear K1; subst. destruct (IHK2 _ _ (eq_refl _)) as [l3 [J1 J2]]. injection J1; clear J1; intros; subst f' l3. exists l1; split; [apply eq_refl | apply refl_trans_clos_is_trans with l2; [right; left | ]; assumption]. destruct K as [l2 [J1 J2]]. subst u2; constructor 1 with l2; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec)