| ⊢ | (f ∧fin w) ≡ f ; w | DiAndFinEqvChopState |
Proof:
1 | ⊢ (f ∧fin w) ; true ≡ f ; (w ∧true) | |
2 | ⊢ w ∧true ≡ w | |
3 | ⊢ f ; (w ∧true) ≡ f ; w | |
4 | ⊢ (f ∧fin w) ; true ≡ f ; w | |
5 | ⊢ (f ∧fin w) ≡ f ; w | 4, def. of |
qed
Here is a corollary of DiAndFinEqvChopState: