Nuprl Lemma : t-sqle_reflexive

[T:Type]. ∀a:T. t-sqle(T;a;a)


Proof




Definitions occuring in Statement :  t-sqle: t-sqle(T;a;b) uall: [x:A]. B[x] all: x:A. B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] t-sqle: t-sqle(T;a;b) squash: T exists: x:A. B[x] per-class: per-class(T;a) prop: subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s] sq_stable: SqStable(P) implies:  Q
Lemmas referenced :  sq_stable__t-sqle base_wf subtype_rel_b-union-right per-class_wf exists_wf sqle_wf_base is-exception_wf has-value_wf_base squash-per-class
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation lemma_by_obid sqequalHypSubstitution isectElimination thin because_Cache hypothesisEquality sqequalRule lambdaEquality dependent_functionElimination imageElimination hypothesis imageMemberEquality baseClosed universeEquality rename dependent_pairFormation divergentSqle sqleReflexivity setElimination cumulativity applyEquality independent_functionElimination

Latex:
\mforall{}[T:Type].  \mforall{}a:T.  t-sqle(T;a;a)



Date html generated: 2016_05_13-PM-04_12_50
Last ObjectModification: 2016_01_14-PM-07_29_11

Theory : subtype_1


Home Index