| ⊢ | (f ; g) ∧fin w ≡ f ; (g ∧fin w) | ChopAndFin |
Proof for ⊃ :
1 | ⊢ fin w ⊃true fin w | |
2 | ⊢ (f ; g) ∧fin w ⊃ (f ; g) ∧true fin w | |
3 | ⊢ (f ; g) ∧true fin w ⊃ f ; (g ∧fin w) | |
4 | ⊢ (f ; g) ∧fin w ⊃ f ; (g ∧fin w) | |
qed
Proof for ⊂:
1 | ⊢ f ; (g ∧fin w) ⊃ f ; g | |
2 | ⊢ f ; (g ∧fin w) ⊃ f ; fin w | |
3 | ⊢ f ; fin w ⊃fin w | |
4 | ⊢ fin w ⊃fin w | |
5 | ⊢ f ; (g ∧fin w) ⊃ (f ; g) ∧fin w | |
qed
Here is a corollary used in some proofs by contradiction: