| ⊢ | f ; f ; … ; f ⊃ f∗ | ChopGroupImpCS |
The proof is by induction on the number of <chops>.
Proof when no <chops>:
1 | ⊢ f ⊃ f∗ |
qed
Proof for at n occurrences of <chops> where n ≥ 1:
1 | ⊢ f ; … ; f ⊃ f∗ | induction for n − 1 <chops> |
2 | ⊢ f ; f ; … ; f ⊃ f ; f∗ | |
3 | ⊢ f ; f∗⊃ f∗ | |
4 | ⊢ f ; f ; … ; f ⊃ f∗ |
qed