⊢ | f ; g ∧ h ⊃ f ; (g ∧ h) | ChopAndBoxImport |
Proof:
1 | ⊢ h ∧ f ; g ⊃ f ; (h ∧ g) | |
2 | ⊢ f ; (h ∧ g) ≡ f ; (g ∧ h) | |
3 | ⊢ h ∧ f ; g ⊃ f ; (g ∧ h) |
qed
The following are easily proved:
⊢ | f ; (g ∧ g1) ⊃ f ; g | ChopAndA |
⊢ | f ; (g ∧ g1) ⊃ f ; g1 | ChopAndB |
⊢ | f ; (g ∧ g1) ≡ f ; (g1 ∧ g) | ChopAndCommute |