In precept, we defined a relation between
two implementations of a range (ListRange
and LoHiPairRange):

let abs (lr:ListRange) (pr:LoHiPairRange) =
     (hd lr , hd (rev lr)) = pr

We also laid out the proof obligation for
showing that the relationship between the
module persists through their APIs:

Forall k:int:
       abs (L.singleton k) (P.singleton k) = true
Forall i,j:int:
       abs (L.range i j) (P.range i j) = true
Forall l:(int list), p:(int*int), k:int:
       if (abs l p) then abs (l*k) (p*k) = true
       if (abs l p) then abs (l+k) (p+k) = true
Forall l1,l2:(int list), p1,p2:(int*int): 
       if (abs l1 p1) and (abs l2 p2) then
       (abs (L.range l1 l2) (P.range p1 p2)) = true

This week's exercise is to complete the proofs.