proposition: Lemma one_step_list_refl_trans_clos_one_step : forall A R (l1 l2 : list A) s k1 k2 t, length l1 = length k1 -> (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. induction H as [u u' k H | u l k' H]. intros l1 l2 s k1 k2 t L H1 H2. destruct l1 as [ | a1 l1]; destruct k1 as [ | b1 k1]. injection H1; injection H2; intros; subst; right; left; trivial. discriminate. discriminate. injection H1; injection H2; intros K1 K2 K3 K4; subst. injection L; clear L; intro L. assert (s_eq_t : s = t). revert L K3; clear. revert l2 s k1 k2 t; induction l1 as [ | a1 l1]; intros l2 s [ | b1 k1] k2 t L H. injection H; intros; subst; trivial. discriminate. discriminate. injection L; clear L; intro L. injection H; intros K1 K2; subst. apply (IHl1 l2 s k1 k2 t); trivial. subst t; left. intros [ | a1 l1] l2 s [ | b1 k1] k2 t L H1 H2. simpl in H1, H2; injection H1; injection H2; intros K1 K2 K3 K4; repeat subst. left. discriminate. discriminate. injection L; clear L; intro L. injection H1; injection H2; intros K1 K2 K3 K4; subst. apply (IHH _ _ _ _ _ _ L (eq_refl _) (eq_refl _)). Qed.
imports: Coq(Setoid Relations List Wellfounded)