// Code we just went through

datatype Option<T> = None | Some(value: T)

datatype BST<K, V> = Leaf
  | Node(key: K, value: V, left: BST<K, V>, right: BST<K, V>)

function Lookup<K(==), V>(lt: (K, K) -> bool, t: BST<K, V>, k: K): Option<V>
{
  match t
  case Leaf => None
  case Node(k', v, l, r) =>
    if k == k' then
      Some(v)
    else if lt(k, k') then
      Lookup(lt, l, k)
    else
      Lookup(lt, r, k)
}

function Mirror<K, V>(t: BST<K, V>): BST<K, V> {
  match t
  case Leaf => Leaf
  case Node(k, v, l, r) => Node(k, v, Mirror(r), Mirror(l))
}

function Flip<A, B, C>(f: (A, B) -> C): (B, A) -> C {
  (b, a) => f(a, b)
}

lemma LookupMirror<K, V>(lt: (K, K) -> bool, t: BST<K, V>, k: K)
  requires forall a, b : K :: lt(a, b) == (!lt(b, a) && a != b)
  ensures Lookup(lt, t, k) == Lookup(Flip(lt), Mirror(t), k)

lemma LookupExtensional<K, V>(lt: (K, K) -> bool, lt': (K, K) -> bool, t: BST<K, V>, k: K)
  requires forall a, b : K :: lt(a, b) == lt'(a, b)
  ensures Lookup(lt, t, k) == Lookup(lt', t, k)

// Your task: prove this lemma

lemma LookupMirrorInt<V>(t: BST<int, V>, k: int)
  ensures Lookup((a, b) => a < b, t, k) == Lookup((b, a) => a < b, Mirror(t), k)