Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

hyp,concl:Formula List. fhyp.( f > 0) fconcl.( f > 0) <hyp, concl> = 0

Applied Tactic: D 0 THENA Auto THEN ListInd (-1)
Generated subgoals:

1. concl:Formula List. f[].( f > 0) fconcl.( f > 0) <[], concl> = 0

2. concl:Formula List. f(u::v).( f > 0) fconcl.( f > 0) <u::v, concl> = 0