proposition: Lemma cons_star : forall R t l t' l', refl_trans_clos (one_step_list (one_step R)) (t'::l') (t::l) -> refl_trans_clos (one_step R) t' t/\ refl_trans_clos (one_step_list (one_step R)) l' l.
proof: Proof. intros R t l t' l' H. set (l1:= t'::l') in *; generalize (eq_refl l1);unfold l1 at 1;clearbody l1. set (l2:= t::l) in *; generalize (eq_refl l2);unfold l2 at 1;clearbody l2. revert t l t' l'. induction H. intros;do 2 subst. injection H0;clear H0;intros;subst. split;constructor. induction H. induction H. intros t l0 t' l' H0 H1. injection H0;injection H1;clear H0 H1. intros;repeat subst. split. constructor 2;constructor;assumption. constructor. intros tk l0 t' l' H0 H1. injection H0;injection H1;clear H0 H1. intros;repeat subst. split. constructor. constructor 2;constructor;assumption. intros t l t' l' H1 H2. subst. inversion H;subst. destruct (IHtrans_clos _ _ _ _ (eq_refl _) (eq_refl _)) as [h1 h2]. clear IHtrans_clos H H0. split. inversion h1;subst;clear h1. constructor. constructor;assumption. constructor. constructor 2 with t2; assumption. assumption. destruct (IHtrans_clos _ _ _ _ (eq_refl _) (eq_refl _)) as [h1 h2]. clear IHtrans_clos H H0. split. assumption. inversion h2;subst;clear h2. constructor. constructor;assumption. constructor. constructor 2 with l2; assumption. Qed.
imports: Coq(List Bool FunInd) CoLoR(weaved_relation closure term_spec terminaison)