pub fn syn_typed_eq(ty: &str, a: Syn, b: Syn) -> Syn
SApp (SApp (SApp (SName "Eq") (SName ty)) a) b — the typed equation try_ring reads.
SApp (SApp (SApp (SName "Eq") (SName ty)) a) b
try_ring