proposition: Lemma rwr_list_chop : forall A R (k1 l1 k2 l2 : list A), length k1 = length k2 -> trans_clos (one_step_list R) (k1 ++ l1) (k2 ++ l2) -> refl_trans_clos (one_step_list R) l1 l2.
proof: Proof. intros A R k1 l1 k2 l2 L H. set (ll1 := k1 ++ l1) in *. assert (H1 := eq_refl ll1). unfold ll1 at 2 in H1. clearbody ll1. set (ll2 := k2 ++ l2) in *. assert (H2 := eq_refl ll2). unfold ll2 at 2 in H2. clearbody ll2. revert k1 l1 k2 l2 L H1 H2. induction H as [ll1 ll2 H | ll1 ll2 ll3 H1 H2]; intros k1 l1 k2 l2 L K1 K2. apply one_step_list_chop with k1 k2; subst; trivial. assert (H : exists k3, exists l3, length k1 = length k3 /\ ll2 = k3 ++ l3). generalize (one_step_list_length_eq H1). subst; clear. revert ll2 l1; induction k1 as [ | a k1]; intros ll2 l1 L. exists nil; exists ll2; split; apply eq_refl. destruct ll2 as [ | b ll2]. discriminate. simpl in L; injection L; clear L; intro L. destruct (IHk1 _ _ L) as [k3 [l3 [L' H]]]; subst. exists (b :: k3); exists l3; split; trivial. simpl; apply f_equal; trivial. destruct H as [k3 [l3 [L' K3]]]. apply refl_trans_clos_is_trans with l3. apply one_step_list_chop with k1 k3; subst; trivial. apply IHH2 with k3 k2; trivial. rewrite <- L'; assumption. Qed.
imports: Coq(Setoid Relations List Wellfounded)