proposition: Lemma refl_trans_clos_one_step_list_length_eq : forall A R (l1 l2 : list A), refl_trans_clos (one_step_list R) l1 l2 -> length l1 = length l2.
proof: Proof. intros A R l1 l2 H; inversion H as [l | k1 k2 K]; clear H; subst. apply eq_refl. apply trans_clos_one_step_list_length_eq with R; assumption. Qed.
imports: Coq(Setoid Relations List Wellfounded)