Solution for Triples.AlternativeExistentialRule.triple_hexists_of_triple_hexists2
introv M.
applys triple_conseq (\exists x, Hof x) (fun (v:val) => \exists (x:A), Q v).
{ applys triple_hexists2. intros x. applys M. } { xsimpl. } { xsimpl. }
(* details:
{ applys himpl_refl. }
{ intros v. applys himpl_hexists_l. intros _. applys himpl_refl. } *)
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
