Solution for Wand.Hand.hand_eq_hand'
applys fun_ext_2. intros H1 H2. unfold hand, hand', hforall.
applys himpl_antisym.
{ intros h N. split. { applys N true. } { applys N false. } }
{ intros h (K1&K2) b. case_if. { applys K1. } { applys K2. } }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
