### Nuprl Lemma : pair-sq-axiom-wf

`∀[a,b:Top].  (<a, b> ~ Ax ∈ Type)`

Proof

Definitions occuring in Statement :  uall: `∀[x:A]. B[x]` top: `Top` member: `t ∈ T` pair: `<a, b>` universe: `Type` sqequal: `s ~ t` axiom: `Ax`
Definitions unfolded in proof :  member: `t ∈ T` uall: `∀[x:A]. B[x]` bfalse: `ff` true: `True` btrue: `tt` ifthenelse: `if b then t else f fi ` assert: `↑b` false: `False` implies: `P `` Q` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` squash: `↓T`
Lemmas referenced :  base_wf top_wf
Rules used in proof :  because_Cache hypothesisEquality thin isectElimination isect_memberEquality lemma_by_obid equalitySymmetry equalityTransitivity axiomEquality sqequalRule hypothesis sqequalHypSubstitution cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution baseClosed closedConclusion baseApply sqequalIntensionalEquality voidElimination natural_numberEquality lambdaFormation universeEquality pointwiseFunctionalityForEquality promote_hyp sqequalExtensionalEquality independent_pairFormation Error :lambdaFormation_alt,  dependent_functionElimination independent_functionElimination Error :universeIsType,  imageMemberEquality

Latex:
\mforall{}[a,b:Top].    (<a,  b>  \msim{}  Ax  \mmember{}  Type)

Date html generated: 2019_06_20-PM-00_38_30
Last ObjectModification: 2018_10_15-PM-10_15_07

Theory : list_0

Home Index