Prev Up
DiEmpty

⊢ empty DiEmpty

Proof:

1
⊢ true
PTL
2
⊢ empty ; true ≡true
EmptyChop
3
⊢ empty ; true
1, 2,Prop
4
⊢ empty
3, def. of 

qed

Prev Up

2024-08-03
Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2024