I'm working on a weird proof system involving reductions in the lambda calculus. I'm thinking of including the following axiom:
forall h q s y.
(λg → g g (q s)) (λ f x → h (f f ∘ q ∘ y) x)
===
(λg → g g s) (λ f x → h (f f ∘ y) (q x))
where ∘ is function composition (and has lower precedence than function application)
Are there some simpler axioms (possibly none at all) I could use instead from which this statement could be proven?
Is there a problem I don't see with making this an axiom?