BaRightChopImpChop

(g g1) f ; g f ; g1 BaRightChopImpChop

Proof:

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

qed

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