proposition: Lemma one_step_list_star_l : forall R l x y, refl_trans_clos (Eqt.one_step R) x y -> refl_trans_clos (one_step_list (Eqt.one_step R)) (x::l) (y::l).
proof: Proof. induction 1. constructor. constructor. induction H. repeat (assumption || constructor). constructor 2 with (y::l). repeat (assumption || constructor). assumption. Qed.
imports: Coq(List Bool FunInd) CoLoR(weaved_relation closure term_spec terminaison)