- { tsr_ant_assoc : forall {x a b c}, Rule [((a,,b),,c) |= x] [(a,,(b,,c)) |= x]
- ; tsr_ant_cossa : forall {x a b c}, Rule [(a,,(b,,c)) |= x] [((a,,b),,c) |= x]
- ; tsr_ant_cancell : forall {x a }, Rule [ [],,a |= x] [ a |= x]
- ; tsr_ant_cancelr : forall {x a }, Rule [a,,[] |= x] [ a |= x]
- ; tsr_ant_llecnac : forall {x a }, Rule [ a |= x] [ [],,a |= x]
- ; tsr_ant_rlecnac : forall {x a }, Rule [ a |= x] [ a,,[] |= x]
+ { tsr_ant_assoc : forall {x a b c}, ND [((a,,b),,c) |= x] [(a,,(b,,c)) |= x]
+ ; tsr_ant_cossa : forall {x a b c}, ND [(a,,(b,,c)) |= x] [((a,,b),,c) |= x]
+ ; tsr_ant_cancell : forall {x a }, ND [ [],,a |= x] [ a |= x]
+ ; tsr_ant_cancelr : forall {x a }, ND [a,,[] |= x] [ a |= x]
+ ; tsr_ant_llecnac : forall {x a }, ND [ a |= x] [ [],,a |= x]
+ ; tsr_ant_rlecnac : forall {x a }, ND [ a |= x] [ a,,[] |= x]