theorem System.exi_tr_of_pred_diff {S T : Type u} {sys : System S T} {p : S → Prop} {s s' : S} (h₁ : sys.Reachable s s') (h₂ : ¬p s) (h₃ : p s') : ∃ (s₁ : S) (s₂ : S) (t : T), sys.Reachable s s₁ ∧ sys.tr s₁ t = some s₂ ∧ sys.Reachable s₂ s' ∧ ¬p s₁ ∧ p s₂

theorem System.eq_of_tree_and_reachable {S T : Type u} {sys : System S T} {s s' : S} [hs : sys.Tree s] (h₁ : sys.Reachable s s') (h₂ : sys.Reachable s' s) : s = s'