proposition: Lemma one_step_list_chop : forall A R (k1 l1 k2 l2 : list A), length k1 = length k2 -> one_step_list R (k1 ++ l1) (k2 ++ l2) -> refl_trans_clos (one_step_list R) l1 l2.
proof: Proof. fix one_step_list_chop 3. intros A R k1 l1 k2 l2 L H. destruct k1 as [ | a k1]; destruct k2 as [ | b k2]. right; left; assumption. discriminate. discriminate. simpl in H; inversion H as [t1 t2 k K | t l1' l2' K]; clear H; subst. assert (J : l1 = l2). simpl in L; injection L; clear L. revert H3; clear. revert k1 k2 l1 l2; fix l1_eq_l2 1. intros [ | a k1] [ | b k2] l1 l2 J L. assumption. discriminate. discriminate. injection J; clear J; intros J _. apply (l1_eq_l2 _ _ _ _ J). injection L; trivial. rewrite J; left. apply one_step_list_chop with k1 k2; trivial. simpl in L; injection L; trivial. Qed.
imports: Coq(Setoid Relations List Wellfounded)