proposition: Lemma rwr_list_expand : forall A R (l l' : list A), trans_clos (one_step_list R) l' l <-> exists t, exists t', exists l1, exists l2, exists l1', exists l2', l = l1 ++ t :: l2 /\ l' = l1' ++ t' :: l2' /\ refl_trans_clos (one_step_list R) l1' l1 /\ trans_clos R t' t /\ refl_trans_clos (one_step_list R) l2' l2.
proof: Proof. intros A R l l'; split; intro H. rewrite rwr_list_expand_strong in H. destruct H as [t [t' [l1 [l2 [l2' [H1 [H2 [H3 H4]]]]]]]]. exists t; exists t'; exists l1; exists l2; exists l1; exists l2'. split; [idtac | split; [idtac | split; [idtac | split]]]; try assumption. left. destruct H as [t [t' [l1 [l2 [l1' [l2' [H1 [H2 [H3 [H4 H5]]]]]]]]]]. destruct H3 as [k1 | k1' k1 K3]. rewrite rwr_list_expand_strong. exists t; exists t'; exists k1; exists l2; exists l2'. split; [idtac | split; [idtac | split]]; assumption. apply trans_clos_is_trans with (k1' ++ t :: l2). rewrite rwr_list_expand_strong. exists t; exists t'; exists k1'; exists l2; exists l2'. split; [idtac | split; [idtac | split]]; try assumption. apply eq_refl. subst l; revert K3; clear; intro K; induction K as [k1 k2 K | k1 k2 k3 K1 K2]. left; induction K as [a1 a2 k K | a k1 k2 K]. left; assumption. right; assumption. apply trans_clos_is_trans with (k2 ++ t :: l2); trivial. left; revert K1; clear; intro K; induction K as [a1 a2 k K | a k1 k2 K]. left; assumption. right; assumption. Qed.
imports: Coq(Setoid Relations List Wellfounded)