proposition: Lemma star_cons : forall R t l t' l', refl_trans_clos (one_step R) t' t -> refl_trans_clos (one_step_list (one_step R)) l' l -> refl_trans_clos (one_step_list (one_step R)) (t'::l') (t::l).
proof: Proof. intros R t l t' l' H H0. apply refl_trans_clos_is_trans with (t::l'). clear H0. induction H. constructor. induction H. apply refl_trans_clos_with_R. constructor;assumption. apply refl_trans_clos_is_trans with (y::l'). apply refl_trans_clos_with_R. constructor;assumption. assumption. clear H;induction H0. constructor. induction H. apply refl_trans_clos_with_R. constructor;assumption. apply refl_trans_clos_is_trans with (t::y). apply refl_trans_clos_with_R. constructor;assumption. assumption. Qed.
imports: Coq(List Bool FunInd) CoLoR(weaved_relation closure term_spec terminaison)