proposition: Theorem inverse_trace_relations_work : forall s tr, refl_trans_1n_trace step init s tr -> R s -> T tr.
proof: Proof. Proof using. intros. find_apply_lem_hyp refl_trans_1n_n1_trace. remember init as s'. induction H. - subst. exfalso. pose R_false_init; auto. - subst. concludes. destruct (R_dec x'); intuition eauto using T_monotonic, refl_trans_n1_1n_trace, R_implies_T. Qed.
imports: Coq(List) Verdi(Net) StructTact(StructTactics)