Fixed-point Elimination in the Intuitionistic Propositional Calculus