Solution for Hprop.Extensionality.predicate_extensionality_derived
introv M. apply functional_extensionality.
intros x. apply propositional_extensionality.
apply M.
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback