Nuprl Lemma : id_perm_wf

T:Type. (id_perm() ∈ Perm(T))


Proof




Definitions occuring in Statement :  id_perm: id_perm() perm: Perm(T) all: x:A. B[x] member: t ∈ T universe: Type
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T id_perm: id_perm() uall: [x:A]. B[x] implies:  Q compose: g identity: Id tidentity: Id{T} inv_funs: InvFuns(A;B;f;g) and: P ∧ Q
Lemmas referenced :  mk_perm_wf_a identity_wf istype-universe
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut sqequalRule introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality isectElimination because_Cache hypothesis independent_functionElimination universeIsType universeEquality functionExtensionality_alt independent_pairFormation

Latex:
\mforall{}T:Type.  (id\_perm()  \mmember{}  Perm(T))



Date html generated: 2019_10_16-PM-00_58_47
Last ObjectModification: 2018_10_08-AM-09_46_33

Theory : perms_1


Home Index