Nuprl Lemma : mk_mFOLProofNode_wf
∀[T:Type]. ∀[sr:mFOL-sequent() × mFOLRule()]. ∀[subgoals:T List]. (srsubgoals ∈ mFOL-sequent() × mFOLRule() × (T List))
Proof
Definitions occuring in Statement :
mk_mFOLProofNode: mk_mFOLProofNode,
mFOL-sequent: mFOL-sequent(),
mFOLRule: mFOLRule(),
list: T List,
uall: ∀[x:A]. B[x],
member: t ∈ T,
product: x:A × B[x],
universe: Type
Lemmas :
list_wf,
mFOL-sequent_wf,
mFOLRule_wf
\mforall{}[T:Type]. \mforall{}[sr:mFOL-sequent() \mtimes{} mFOLRule()]. \mforall{}[subgoals:T List].
(sr
subgoals \mmember{} mFOL-sequent() \mtimes{} mFOLRule() \mtimes{} (T List))
Date html generated:
2015_07_17-AM-07_56_51
Last ObjectModification:
2015_01_27-AM-10_05_07
Home
Index