Solution for Repr.triple_mlength_using_miter
xwp. xapp. intros c. xfun. intros f Hf.
xapp (triple_miter (fun (K:list val) => c ~~> (length K))).
{ intros x K L' ->. xapp. xapp. xsimpl*. { rew_list. math. } }
clear Hf. xapp. xsimpl*.
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
