//@ [coq,fstar] subdir=misc
struct AVLNode<T> {
    value: T,
    left: AVLTree<T>,
    right: AVLTree<T>,
}

type AVLTree<T> = Option<Box<AVLNode<T>>>;

fn get_val<T>(x: AVLNode<T>) -> T {
    x.value
}

fn get_left<T>(x: AVLNode<T>) -> AVLTree<T> {
    x.left
}