Level: Lib Thy Top: 1
Hypotheses:

  1. e :

  2. L : List

  3. n :

Conclusion:

||e:(Ln)|| = n * ||e:L||

Applied Tactic: NatInd 3
Generated subgoals:

1. ||e:(L0)|| = 0 * ||e:L||

2. ||e:(Ln)|| = n * ||e:L||