no goals
α : Type u_2
β : Type u_1
γ : Type ?u.23283
δ : Type ?u.23286
r : α → α → Prop
a✝ b✝ c d : α
p : β → β → Prop
a b : α
f : α → β
h : ∀ (a b : α), r a b → TransGen p (f a) (f b)
hab : TransGen r a b
⊢ TransGen p (f a) (f b)
simpa [transGen_idem] using hab.lift f h