proposition: Lemma refl_trans_1n_n1_trace : forall step x y l, refl_trans_1n_trace step x y l -> refl_trans_n1_trace step x y l.
proof: Proof. Proof using. intros. induction H. - constructor. - eapply RTn1_step; eauto. Qed.
imports: Coq(List) StructTact(StructTactics) StructTact(Update Update2 RemoveAll) Coq(Sumbool Relation_Definitions RelationClasses) Cheerios(Cheerios)