Nuprl Lemma : tag-by-subtype-tag-case

[T,S:Type].  ∀z,x:Atom.  (z×T ⊆x:S ⇐⇒ (¬↑=a x) ∨ (T ⊆S))


Proof




Definitions occuring in Statement :  tag-by: T tag-case: z:T assert: b eq_atom: =a y subtype_rel: A ⊆B uall: [x:A]. B[x] all: x:A. B[x] iff: ⇐⇒ Q not: ¬A or: P ∨ Q atom: Atom universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] member: t ∈ T implies:  Q bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a assert: b ifthenelse: if then else fi  iff: ⇐⇒ Q or: P ∨ Q subtype_rel: A ⊆B rev_implies:  Q not: ¬A true: True false: False bfalse: ff exists: x:A. B[x] sq_type: SQType(T) guard: {T} bnot: ¬bb tag-by: T tag-case: z:T prop: so_lambda: λ2x.t[x] so_apply: x[s] nequal: a ≠ b ∈  top: Top pi2: snd(t) pi1: fst(t)
Lemmas referenced :  eq_atom_wf eqtt_to_assert assert_of_eq_atom eqff_to_assert bool_cases_sqequal subtype_base_sq bool_wf bool_subtype_base assert-bnot neg_assert_of_eq_atom istype-void subtype_rel_wf tag-by_wf tag-case_wf subtype_rel_product equal-wf-base atom_subtype_base ifthenelse_wf top_wf istype-atom istype-universe subtype_rel-equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt lambdaFormation_alt cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis inhabitedIsType unionElimination equalityElimination equalityTransitivity equalitySymmetry productElimination independent_isectElimination sqequalRule independent_pairFormation inrFormation_alt lambdaEquality_alt universeIsType because_Cache independent_functionElimination natural_numberEquality voidElimination axiomEquality dependent_pairFormation_alt equalityIstype promote_hyp dependent_functionElimination instantiate cumulativity inlFormation_alt setEquality atomEquality applyEquality setIsType universeEquality setElimination rename isect_memberEquality_alt unionIsType functionIsType dependent_set_memberEquality_alt productIsType applyLambdaEquality sqequalBase independent_pairEquality

Latex:
\mforall{}[T,S:Type].    \mforall{}z,x:Atom.    (z\mtimes{}T  \msubseteq{}r  x:S  \mLeftarrow{}{}\mRightarrow{}  (\mneg{}\muparrow{}z  =a  x)  \mvee{}  (T  \msubseteq{}r  S))



Date html generated: 2019_10_15-AM-11_29_46
Last ObjectModification: 2019_06_25-PM-01_21_26

Theory : general


Home Index