Solution for WPgen.ProofsWithXtactics.triple_succ_using_incr_with_xtactics
xwp.
xapp_nosubst triple_ref. intros ? p ->.
xapp_nosubst triple_incr.
xapp_nosubst triple_get. intros ? ->.
xapp_nosubst triple_free.
xval. xsimpl. auto.
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback