Investigate whether using `context` tactic to express proof mode tactics makes them more efficient (compared to computation)

[berpeti]

• This issue came up when defining mlConj with mlAssert