Term
val is_normal : Ast.term -> bool
Test if a term is in normal form for CBV
val is_neutral : Ast.term -> bool
Test if a term is neutral in CBV; This is not the exact definition of neutral. Here, we mean a term whose type in known with elimination or type decocation applied to it