proposition: Lemma one_step_list_star_decompose_nil : forall R l'', refl_trans_clos (one_step_list (Eqt.one_step R)) nil l'' -> l'' = nil.
proof: Proof. intros R l'' H. set (l:= @nil Eqt.T.term) in *. generalize (eq_refl l). unfold l at 1;clearbody l. induction H;intro;subst;auto. inversion H;clear H;subst; inversion H0. Qed.
imports: Coq(List Bool FunInd) CoLoR(weaved_relation closure term_spec terminaison)