Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

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

Applied Tactic: UnivCD THENW Auto
Generated subgoals:

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