Solution for Repr.triple_miter
introv Hf.
cuts G: (forall L1 L2, L = L1++L2 ->
triple (miter f p)
(MList L2 p \* I L1)
(fun u => MList L2 p \* I L)).
{ apply G. rew_list*. }
intros L1 L2 E. gen p L1. induction_wf IH: list_sub L2; intros.
xwp. xapp. xchange MList_if. xif; intros C; case_if; xpull.
{ intros x q L' ->. xapp. xapp. xapp. xapp.
{ constructors. } { rew_list* in *. } xchange <- MList_cons. }
{ intros ->. xval. rew_list in *. subst. xchanges* <- (MList_nil null). }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
