| ⊢ (skip ∧ T) ≡more ∧ T | DfSkipAndNLoneEqvMoreAndNLone |
Proof:
1 | finite ⊃ (skip ∧ T) ≡ (more ∧ T) | |
2 | (skip ∧ T) ≡ (more ∧ T) | |
3 | (skip ∧ T) ≡ (skip ∧ T) | |
4 | (more ∧ T) ≡more ∧ T | |
5 | (skip ∧ T) ≡more ∧ T |
qed