proposition: Lemma refl_trans_clos_one_step_list_head_tail : forall A R s t (l1 l2 : list A), refl_trans_clos (one_step_list R) (s :: l1) (t :: l2) <-> (refl_trans_clos R s t /\ refl_trans_clos (one_step_list R) l1 l2).
proof: Proof. intros A R s t l1 l2; split; intro H. inversion H as [l | l1' l2' H']; clear H; subst. split; left. set (k1 := s :: l1) in *; assert (H1 := eq_refl k1); unfold k1 at 2 in H1; clearbody k1. set (k2 := t :: l2) in *; assert (H2 := eq_refl k2); unfold k2 at 2 in H2; clearbody k2. revert s t l1 l2 H1 H2. induction H' as [k1 k2 H | k1 k2 k3 H]. intros s t l1 l2 H1 H2; subst; inversion H; clear H; subst; split. right; left; assumption. left. left. right; left; assumption. intros s t l1 l2 H1 H2; subst. inversion H; clear H; subst. destruct (IHH' t2 t l1 l2) as [H1 H2]; trivial. split. apply refl_trans_clos_is_trans with t2; [right; left | idtac]; assumption. assumption. destruct (IHH' s t l3 l2) as [H1 H2]; trivial. split. assumption. apply refl_trans_clos_is_trans with l3. right; left; assumption. assumption. destruct H as [H1 H2]. apply refl_trans_clos_is_trans with (s :: l2). inversion H2 as [l | k1 k2 K2]; clear H2; subst. left. right; induction K2. left; right; assumption. apply trans_clos_is_trans with (s :: y); trivial. left; right; assumption. inversion H1 as [u | s' t' K1]; clear H1; subst. left. induction K1. right; do 2 left; assumption. apply refl_trans_clos_is_trans with (y :: l2); trivial. right; do 2 left; assumption. Qed.
imports: Coq(Setoid Relations List Wellfounded)