Diamond

theorem diamond {ps : Set P} {s s1 s2 : State P M S}    (h1 : a.CanReachVia ps s s1) (h2 : a.CanReachVia psᶜ s s2) :    ∃ s', a.CanReachVia psᶜ s1 s' ∧ a.CanReachVia ps s2 s' := by  obtain ⟨xs1, h_mtr1, h_via1⟩ := h1  induction h_mtr1 generalizing s2  case refl s =>    use s2    simp_all [refl]  case stepL s x t1 xs s1 h_tr1 h_mtr1 h_ind =>    obtain ⟨h_x, h_xs⟩ := (List.forall_cons (DestIn ps) x xs).mp h_via1    obtain ⟨t2, h_crv, h_tr2⟩:= diamond_helper h_x h_tr1 h2    obtain ⟨s', h_crv1, h_crv2⟩ := h_ind h_crv h_xs    use s', h_crv1    exact stepL h_x h_tr2 h_crv2