Solution for WPgen.ProofsWithXlemmas.triple_succ_using_incr_with_xlemmas
intros.
applys xwp_lemma. { reflexivity. }
simpl; unfold wpgen_var; simpl.
applys xstruct_lemma.
applys xlet_lemma.
applys xstruct_lemma.
applys xapp_lemma. { apply triple_ref. } { xsimpl. }
xpull; intros ? p ->.
applys xstruct_lemma.
applys xseq_lemma.
applys xstruct_lemma.
applys xapp_lemma. { apply triple_incr. } { xsimpl. }
intros ?.
applys xstruct_lemma.
applys xlet_lemma.
applys xstruct_lemma.
applys xapp_lemma. { apply triple_get. } { xsimpl. }
xpull; intros ? ->.
applys xstruct_lemma.
applys xseq_lemma.
applys xstruct_lemma.
applys xapp_lemma. { apply triple_free. } { xsimpl. }
intros ?.
applys xstruct_lemma.
applys xval_lemma.
xsimpl. auto.
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
