Solution for Repr.triple_tree_copy
intros. gen p. induction_wf IH: tree_sub T.
xwp. xapp. xchange MTree_if. xif; intros C; case_if; xpull.
{ intros E. xval. do 2 xchange* <- (MTree_Leaf null). subst. xsimpl*. }
{ intros n p1 p2 T1 T2 ->. xapp. xapp. xapp.
xapp. { constructors. } intros q1.
xapp. { constructors. } intros q2.
xapp. intros q. xchange <- MTree_Node. subst. xsimpl*. }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
