no goals
α : Type u_1
β : Type u_2
γ : Type ?u.314
f fab : α → β
fbc : β → γ
ga ga' : α → α
gb gb' : β → β
gc gc' : γ → γ
h : Semiconj f ga gb
h' : Semiconj f ga' gb'
x : α
⊢ f ((ga ∘ ga') x) = (gb ∘ gb') (f x)
simp only [comp_apply, h.eq, h'.eq]