PrintForm Definitions action sets Sections AutomataTheory Doc

At: counter append 1 1
1. e:
2. L: *
3. M: *

||e:nil @ M|| = ||e:nil||+||e:M||
By: RecCaseSplit `append`
Generated subgoal:

1 ||e:M|| = ||e:nil||+||e:M||

About:
equalniladdintlist