Comment by nextaccountic

That's how F* (FStar) works, right? You may write out proof objects manually but most of time they are inferred by SMT