Solution for Hprop.Extensionality.predicate_extensionality_derived
Click on the 'Next' button to reveal the proof step by step.