Nuprl Lemma : mRuleorI_wf
∀[left:𝔹]. (mRuleorI(left) ∈ mFOLRule())
Proof
Definitions occuring in Statement : 
mRuleorI: mRuleorI(left)
, 
mFOLRule: mFOLRule()
, 
bool: 𝔹
, 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
mFOLRule: mFOLRule()
, 
mRuleorI: mRuleorI(left)
, 
eq_atom: x =a y
, 
ifthenelse: if b then t else f fi 
, 
bfalse: ff
, 
btrue: tt
Lemmas referenced : 
ifthenelse_wf, 
eq_atom_wf, 
unit_wf2, 
bool_wf, 
nat_wf
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
isect_memberFormation_alt, 
cut, 
sqequalRule, 
dependent_pairEquality_alt, 
tokenEquality, 
hypothesisEquality, 
universeIsType, 
thin, 
instantiate, 
introduction, 
extract_by_obid, 
sqequalHypSubstitution, 
isectElimination, 
hypothesis, 
universeEquality, 
intEquality, 
productEquality, 
voidEquality
Latex:
\mforall{}[left:\mBbbB{}].  (mRuleorI(left)  \mmember{}  mFOLRule())
Date html generated:
2020_05_20-AM-09_08_55
Last ObjectModification:
2020_01_24-PM-02_00_56
Theory : minimal-first-order-logic
Home
Index