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