| ⊢ | 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 |