Nuprl Lemma : sqequaln_symm
∀[a,b:Base]. ∀[n:ℕ]. a ~n b supposing b ~n a
Proof
Definitions occuring in Statement :
nat: ℕ,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
base: Base,
sqequal_n: s ~n t
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
uimplies: b supposing a,
member: t ∈ T
Lemmas referenced :
sqequal_n_wf,
nat_wf,
base_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :isect_memberFormation_alt,
sqequalnSymm,
hypothesis,
Error :universeIsType,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
Error :inhabitedIsType
Latex:
\mforall{}[a,b:Base]. \mforall{}[n:\mBbbN{}]. a \msim{}n b supposing b \msim{}n a
Date html generated:
2019_06_20-AM-11_33_52
Last ObjectModification:
2018_10_15-PM-05_04_25
Theory : int_1
Home
Index