pub fn confluence_ty() -> Expr
Confluence: the reflexive transitive closure of →β has the diamond property