⊢ f ≡ f | DfDfEqvDf |
Proof:
1 | (f ⌢ true) ⌢ true ≡ f ⌢ (true ⌢ true) | |
2 | true ≡true | |
3 | (true ⌢ true) ≡true | 2, def. of |
4 | f ⌢ (true ⌢ true) ≡ f ⌢ true | |
5 | (f ⌢ true) ⌢ true ≡ f ⌢ true | |
6 | f ≡ f | 5, def. of |
qed