proposition: Lemma star_list : forall R f l l', refl_trans_clos (one_step_list (one_step R)) l' l -> refl_trans_clos (one_step R) (Term f l') (Term f l).
proof: Proof. intros R f l l' H. induction H. constructor. constructor. induction H. constructor. constructor 2;assumption. constructor 2 with (Eqt.T.Term f y). constructor 2;assumption. assumption. Qed.
imports: Coq(List Bool FunInd) CoLoR(weaved_relation closure term_spec terminaison)