proposition: Lemma refl_trans_1n_trace_n1_ind : forall (step : step_relation) (P : A -> A -> list trace -> Prop), (forall x, P x x []) -> (forall x x' x'' tr1 tr2, refl_trans_1n_trace step x x' tr1 -> step x' x'' tr2 -> P x x' tr1 -> refl_trans_1n_trace step x x'' (tr1 ++ tr2) -> P x x'' (tr1 ++ tr2)) -> forall x y l, refl_trans_1n_trace step x y l -> P x y l.
proof: Proof. Proof using. intros. find_apply_lem_hyp refl_trans_1n_n1_trace. eapply refl_trans_n1_trace_ind; eauto. intros. eapply H0; eauto using refl_trans_n1_1n_trace, RT1n_step. Qed.
imports: Coq(List) StructTact(StructTactics) StructTact(Update Update2 RemoveAll) Coq(Sumbool Relation_Definitions RelationClasses) Cheerios(Cheerios)