Nuprl Lemma : ycomb_wf_trivial
Y ∈ Void ⟶ Void
Proof
Definitions occuring in Statement : 
ycomb: Y
, 
member: t ∈ T
, 
function: x:A ⟶ B[x]
, 
void: Void
Definitions unfolded in proof : 
member: t ∈ T
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
functionExtensionality, 
voidElimination, 
voidEquality
Latex:
Y  \mmember{}  Void  {}\mrightarrow{}  Void
Date html generated:
2019_06_20-AM-11_19_40
Last ObjectModification:
2018_12_07-PM-02_14_20
Theory : sqequal_1
Home
Index