Solution for Triples.AlternativeExistentialRule.triple_hexists2
introv M. applys triple_hexists. intros x.
applys triple_conseq (M x); xsimpl.
(* details:
{ applys himpl_refl. }
{ intros v. applys himpl_hexists_r x. applys himpl_refl. } *)
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
