proposition: Lemma one_step_list_same_length : forall R l1 l2, one_step_list (Eqt.one_step R) l2 l1 -> length l1 = length l2.
proof: Proof. intros R l1 l2 H; apply sym_eq; apply one_step_list_length_eq with (Eqt.one_step R); assumption. Qed.
imports: Coq(List Bool FunInd) CoLoR(weaved_relation closure term_spec terminaison)