Level: Lib Thy Top:
Hypotheses:None
Conclusion:
T:
. x:
. as:T List. x < ||as|| 
firstn(x + 1;as) = firstn(x;as) @ (as[x]::[])
Applied Tactic: (D 0 THENM D 0 ...a)
Generated subgoals:1. as:T List. x < ||as|| firstn(x + 1;as) = firstn(x;as) @ (as[x]::[])