∀[T:Type]. ∀[sr:mFOL-sequent() × FOLRule()]. ∀[subgoals:T List]. (sr
subgoals ∈ mFOL-sequent() × FOLRule() × (T List))
{ ProveWfLemma }