Function exists_term 

pub fn exists_term(term: PTerm) -> Tactic

exists <term> as a tactic value, with the witness resolved against the goal’s scope.