Solution for Wand.Hor.hor_eq_hor'
applys fun_ext_2. intros H1 H2. unfold hor, hor'. applys himpl_antisym.
{ xsimpl. intros b h K. destruct b. { left*. } { right*. } }
{ intros h K. destruct K. { exists* true. } { exists* false. } }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
