proposition: Lemma trans_clos_one_step_list_length_eq : forall A R (l1 l2 : list A), trans_clos (one_step_list R) l1 l2 -> length l1 = length l2.
proof: Proof. intros A R l1 l2 H; induction H as [l1 l2 H | l1 l2 l3 H1 H2]. apply one_step_list_length_eq with R; assumption. rewrite (one_step_list_length_eq H1); assumption. Qed.
imports: Coq(Setoid Relations List Wellfounded)