- { 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]
+ { 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]