proposition: Lemma one_step_list_refl_trans_clos : forall R l l' x y, refl_trans_clos (Eqt.one_step R) x y -> refl_trans_clos (one_step_list (Eqt.one_step R)) l l' -> refl_trans_clos (one_step_list (Eqt.one_step R)) (x::l) (y::l').
proof: Proof. intros R l l' x y H H0. apply refl_trans_clos_is_trans with (x::l'). apply one_step_list_star_r. assumption. apply one_step_list_star_l. assumption. Qed.
imports: Coq(List Bool FunInd) CoLoR(weaved_relation closure term_spec terminaison)