proposition: Lemma one_step_list_star_decompose_cons : forall R x l l'', refl_trans_clos (one_step_list (Eqt.one_step R)) (x::l) l'' -> exists x', exists l', l'' = x'::l' /\ refl_trans_clos (Eqt.one_step R) x x'/\ refl_trans_clos (one_step_list (Eqt.one_step R)) l l'.
proof: Proof. intros R x l l''. set (l1 := x::l) in *. generalize (eq_refl l1); unfold l1 at 1;clearbody l1. intros H H0 . revert x l H. induction H0. rename x into l0. intros x l He;subst. exists x;exists l;repeat split;constructor. rename x into l';rename y into l. induction H. inversion H;clear H;subst. intros a b Heq;injection Heq;clear Heq;intros;subst. exists t2;exists l. repeat (assumption||constructor). intros a b Heq;injection Heq;clear Heq;intros;subst. exists t;exists l2. repeat (assumption||constructor). inversion H;clear H;subst; intros; injection H;clear H;intros;subst. destruct (IHtrans_clos _ _ (eq_refl _)) as [u [l'' [h1 [h2 h3]]]];clear IHtrans_clos. subst. exists u;exists l''. split. apply eq_refl. split. apply refl_trans_clos_is_trans with t2; repeat (assumption||constructor). assumption. destruct (IHtrans_clos _ _ (eq_refl _)) as [u [l'' [h1 [h2 h3]]]];clear IHtrans_clos. subst. exists u;exists l''. split. apply eq_refl. split. assumption. apply refl_trans_clos_is_trans with l2; repeat (assumption||constructor). Qed.
imports: Coq(List Bool FunInd) CoLoR(weaved_relation closure term_spec terminaison)