Macro eqx 

macro_rules! eqx {
    (def $x:ident) => { ... };
    ($x:expr, $def:expr, cl, $($cmd:tt),+) => { ... };
    ($x:expr, $def:expr, cr, $($cmd:tt),+) => { ... };
    ($x:expr, $def:expr, am, $($cmd:tt),+) => { ... };
    ($x:expr, $def:expr, a, $($cmd:tt),+) => { ... };
    ($x:expr, $def:expr, $cmd0:tt, $($cmd:tt),+) => { ... };
    ($x:expr, $def:expr, eq) => { ... };
    ($x:expr, $def:expr, l) => { ... };
    ($x:expr, $def:expr, r) => { ... };
    ($x:expr, $def:expr, co) => { ... };
    ($x:expr, $def:expr, tyl) => { ... };
    ($x:expr, $def:expr, tyr) => { ... };
}

Helps converting equality.

• def <id>: Produces an equality that maps a struct to its inner definition
• <expr>, <def>, [<branch cmd>], <leaf cmd>: Applies branch commands and leaf command.

Branch commands

• cl: Compose left
• cr: Compose right
• a: Application argument
• am: Application map

Leaf commands

• eq: Both sides of equality
• l: Left side of equality
• r: Right side of equality
• co: Is-constant argument
• tyl: Type left argument
• tyr: Type right argument