Function term_of_syn 

pub fn term_of_syn(s: &Syn) -> Term

The same reflected syntax as a kernel Term, so a caller can hand the FIRST kernel exactly the goal it handed this module — which is what makes a differential between the two a differential and not two different questions.