ReflTransGen equivalent of TransGen.closed'

Stream: Is there code for X?

[Maja Kądziołka]

I have r a b -> P a -> P b and I would like to obtain ReflTransGen r a b -> P a -> P b. do we have that? for TransGen there's TransGen.closed', which would suffice when combined with TransGen.swap, but there doesn't seem to be an equivalent for ReflTransGen. is the API just not orthogonal for no reason, or am I missing something here?

[Robin Arnez]

Not sure about the API but if you want a proof:

theorem Relation.ReflTransGen.closed'
    (r : α → α → Prop) {P : α → Prop} (h : ∀ a b, r a b → P b → P a) {a b : α}
    (h' : ReflTransGen r a b) : P b → P a := by
  induction h' with
  | refl => exact id
  | tail h' rel ih =>
    exact ih ∘ h _ _ rel