for @{ 'xforall2 ${default
@{\lambda ${ident i1} : $ty1. \lambda ${ident i2} : $ty2. $p}
@{\lambda ${ident i1}, ${ident i2}. $p}}}.
for @{ 'xforall2 ${default
@{\lambda ${ident i1} : $ty1. \lambda ${ident i2} : $ty2. $p}
@{\lambda ${ident i1}, ${ident i2}. $p}}}.