Solution for Basic.triple_step_transfer
intros q p n m Hm.
gen n Hm. induction_wf IH: (downto 0) m. unfold downto in IH.
intros. xwp. xapp. xapp. xif; intros C.
{ xapp. xapp. xapp. { math. } { math. } xsimpl. math. }
{ xval. xsimpl. { math. } { math. } }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
