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