Build a pair. Derive the shortcut.
A asks for two pieces of evidence. Its three primitive rules are enough to derive useful shortcuts without adding authority to the .
1. Three primitive rules
Introduction: from Γ ⊢ p : A and Γ ⊢ q : B, conclude Γ ⊢ andIntro(p, q) : A ∧ B. Both branches are checked in the same ; a temporary assumption in one branch cannot leak into the other.
Left elimination: from Γ ⊢ p : A ∧ B, conclude Γ ⊢ andLeft(p) : A. Right elimination similarly concludes Γ ⊢ andRight(p) : B. Both projections first check that p really establishes a conjunction.
2. An ordinary derived helper
Assume pair : A ∧ B. Extract B with andRight(pair), extract A with andLeft(pair), and combine them with andIntro. Discharging pair proves the implication above.
The commute(pair) builds exactly those primitive . Expand it in the playground to inspect the actual tree and checking trace. There is no commute rule in the kernel.
3. Why the order still matters
A ∧ B and B ∧ A are different proposition trees. Structural equality does not swap them. Commutativity needs a proof, even though its construction is short.
A candidate that returns the original pair unchanged is rejected when the goal asks for the swapped pair. Projecting from a proof of A alone is also rejected: it is not pair evidence.
4. Try the complete flow
In the playground, compare the left projection, right projection, pair-building, and commutativity examples. Inspect the AST separately from the proof AST, then press Check proof.
Hover over or focus any operator in the theorem to underline its complete arguments. For nested formulas, this shows which subexpressions belong to that particular operator.
5. Take this with you
A derived helper can save typing while producing the same primitive evidence. Its output still needs independent ; convenience does not enlarge the trusted kernel.