Nuprl Lemma : alg_one_wf

A:Type. ∀a:algebra_sig{i:l}(A).  (a.one ∈ a.car)


Proof




Definitions occuring in Statement :  alg_one: a.one alg_car: a.car algebra_sig: algebra_sig{i:l}(A) all: x:A. B[x] member: t ∈ T universe: Type
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T algebra_sig: algebra_sig{i:l}(A) alg_one: a.one alg_car: a.car pi1: fst(t) pi2: snd(t)
Lemmas referenced :  algebra_sig_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut sqequalHypSubstitution productElimination thin sqequalRule hypothesisEquality hypothesis lemma_by_obid dependent_functionElimination universeEquality

Latex:
\mforall{}A:Type.  \mforall{}a:algebra\_sig\{i:l\}(A).    (a.one  \mmember{}  a.car)



Date html generated: 2016_05_16-AM-07_26_08
Last ObjectModification: 2015_12_28-PM-05_08_07

Theory : algebras_1


Home Index