proposition: Theorem trace_relations_work : forall s tr, refl_trans_1n_trace step init s tr -> T tr -> R s.
proof: Proof. Proof using. intros. find_copy_apply_lem_hyp refl_trans_1n_n1_trace. remember init as s'. induction H1. - intros; exfalso; pose T_false_init; auto. - subst. destruct (T_dec cs); intuition eauto using R_monotonic, refl_trans_n1_1n_trace, T_implies_R. Qed.
imports: Coq(List) Verdi(Net) StructTact(StructTactics)