| ⊢ | (fin w) ; f ≡ (w ∧ f) ∨ ((fin w) ; f) | FinChopEqvOr |
Proof:
1 | ⊢ fin w ≡ (w ∧empty) ∨fin w | |
2 | ⊢ (fin w) ; f ≡ ((w ∧empty) ∨fin w) ; f | |
3 | ⊢ ((w ∧empty) ∨fin w) ; f ≡ (w ∧empty) ; f ∨ ( fin w) ; f | |
4 | ⊢ (w ∧empty) ; f ≡ w ∧ f | |
5 | ⊢ ( fin w) ; f ≡ ((fin w) ; f) | |
6 | ⊢ (fin w) ; f ≡ (w ∧ f) ∨ ((fin w) ; f) |
qed