T310c
Premises:
(forall ?X (=> (f ?X) (exists ?Y (and (= ?Y ?X) (f ?Y)))))
Conclusion:
(forall ?X (=> (exists ?Y (and (= ?Y ?X) (f ?Y))) (f ?X)))
Proof Trace