Nuprl Lemma : ctt-tokens_wf
ctt-tokens() ∈ Atom List
Proof
Definitions occuring in Statement :
ctt-tokens: ctt-tokens(),
list: T List,
member: t ∈ T,
atom: Atom
Definitions unfolded in proof :
ctt-tokens: ctt-tokens(),
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
cons_wf,
nil_wf
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
atomEquality,
tokenEquality,
hypothesis
Latex:
ctt-tokens() \mmember{} Atom List
Date html generated:
2020_05_20-PM-08_16_04
Last ObjectModification:
2020_05_07-PM-03_12_22
Theory : cubical!type!theory
Home
Index