proposition: Lemma refl_trans_clos_one_step_list_refl_trans_clos_one_step : forall A R (l1 l2 : list A) s k1 k2 t, length l1 = length k1 -> refl_trans_clos (one_step_list R) (l1 ++ s :: l2) (k1 ++ t :: k2) -> refl_trans_clos R s t.
proof: Proof. intros A R l1 l2 s k1 k2 t L H. set (l := l1 ++ s :: l2) in *. assert (H1 := eq_refl l); unfold l at 2 in H1; clearbody l. set (k := k1 ++ t :: k2) in *. assert (H2 := eq_refl k); unfold k at 2 in H2; clearbody k. revert l1 l2 s k1 k2 t L H1 H2. inversion H as [l' | l' k' H']. subst l' k; intros l1 l2 s k1 k2 t L H1 H2. rewrite H2 in H1; clear H2. assert (s_eq_t : s = t). revert k1 s t k2 l2 L H1; induction l1 as [ | a1 l1]; intros [ | b1 k1] s t k2 l2 L H1. injection H1; intros; subst; trivial. discriminate. discriminate. injection L; clear L; intro L. injection H1; intros; subst. apply (IHl1 _ s t k2 l2 L H0). subst t; left. subst l' k'; clear H. induction H' as [l' k' H | l' ll k' H H']. intros l1 l2 s k1 k2 t L H1 H2. subst l' k'; apply (one_step_list_refl_trans_clos_one_step (R := R) l1 l2 s k1 k2 t); trivial. intros l1 l2 s k1 k2 t L H1 H2. assert (L' : length l' = length ll). apply one_step_list_length_eq with R; trivial. assert (H'' : exists ll1, exists ll2, exists u, length l1 = length ll1 /\ ll = ll1 ++ u :: ll2). rewrite H1 in L'. revert L'; clear. revert ll l2 s; induction l1 as [ | a1 l1]; intros ll l2 s L. destruct ll as [ | u ll]. discriminate. exists nil; exists ll; exists u; split; trivial. destruct ll as [ | a ll]. discriminate. injection L; clear L; intro L. destruct (IHl1 _ _ _ L) as [ll1 [ll2 [u [L' H]]]]. exists (a :: ll1); exists ll2; exists u; repeat split. simpl; rewrite L'; trivial. simpl; rewrite H; trivial. destruct H'' as [ll1 [ll2 [u [L'' H'']]]]. apply refl_trans_clos_is_trans with u. apply (one_step_list_refl_trans_clos_one_step (R := R) l1 l2 s ll1 ll2 u); trivial. subst l' ll; assumption. apply (IHH' ll1 ll2 u k1 k2 t); trivial. rewrite <- L''; assumption. Qed.
imports: Coq(Setoid Relations List Wellfounded)