Nuprl Lemma : mon_htfor_nil_lemma

f,g,T:Top.  (HTFor{g} h::t ∈ []. f[h;t] e)


Proof




Definitions occuring in Statement :  mon_htfor: HTFor{g} h::t ∈ as. f[h; t] nil: [] top: Top so_apply: x[s1;s2] all: x:A. B[x] sqequal: t grp_id: e
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T mon_htfor: HTFor{g} h::t ∈ as. f[h; t] so_lambda: λ2y.t[x; y] top: Top so_apply: x[s1;s2]
Lemmas referenced :  top_wf for_hdtl_nil_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut hypothesis lemma_by_obid sqequalRule sqequalHypSubstitution dependent_functionElimination thin isect_memberEquality voidElimination voidEquality

Latex:
\mforall{}f,g,T:Top.    (HTFor\{g\}  h::t  \mmember{}  [].  f[h;t]  \msim{}  e)



Date html generated: 2016_05_16-AM-07_36_36
Last ObjectModification: 2015_12_28-PM-05_45_34

Theory : list_2


Home Index