Solution for Basic.triple_transfer_aliased
Lemma triple_transfer_aliased : forall (p:loc) (n:int),
triple (transfer p p)
(p ~~> n)
(fun _ => p ~~> 0).
Proof using.
xwp. xapp. xapp. xapp. xapp. xapp. xsimpl.
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback