Splice.Macro
val tp_pequiv_in_v : r:D.dim -> pcode:D.con -> code:D.con -> S.tp t
val commute_split : D.con -> D.cof list -> (S.t TB.m -> S.t TB.m) -> S.t t