encoding of match expressions; revised axioms for int/bool/string/unit; sf-basic.fst now verifies