EmptyOrNextChopEqv

(empty f) ; g g (f ; g) EmptyOrNextChopEqv

Proof:

1
(empty f) ; g g (( f) ; g)
2
( f) ; g (f ; g)
3
(empty f) ; g g (f ; g)
1, 2,Prop

qed

2023-09-12
Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2023