Nuprl Lemma : case-term-equal-right

[Gamma:j⊢]. ∀[phi,psi:{Gamma ⊢ _:𝔽}]. ∀[A:{Gamma, (phi ∨ psi) ⊢ _}]. ∀[u:{Gamma, phi ⊢ _:A}]. ∀[v:{Gamma, psi ⊢ _:A}].
  Gamma, psi ⊢ (u ∨ v)=v:A supposing Gamma, (phi ∧ psi) ⊢ u=v:A


Proof




Definitions occuring in Statement :  case-term: (u ∨ v) same-cubical-term: X ⊢ u=v:A context-subset: Gamma, phi face-or: (a ∨ b) face-and: (a ∧ b) face-type: 𝔽 cubical-term: {X ⊢ _:A} cubical-type: {X ⊢ _} cubical_set: CubicalSet uimplies: supposing a uall: [x:A]. B[x]
Definitions unfolded in proof :  uall: [x:A]. B[x] uimplies: supposing a same-cubical-term: X ⊢ u=v:A member: t ∈ T subtype_rel: A ⊆B all: x:A. B[x] implies:  Q iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q or: P ∨ Q bdd-distributive-lattice: BoundedDistributiveLattice so_lambda: λ2x.t[x] prop: so_apply: x[s] guard: {T} context-subset: Gamma, phi case-term: (u ∨ v) cubical-term-at: u(a) cubical-type-at: A(a) pi1: fst(t) face-type: 𝔽 constant-cubical-type: (X) I_cube: A(I) functor-ob: ob(F) face-presheaf: 𝔽 lattice-point: Point(l) record-select: r.x face_lattice: face_lattice(I) face-lattice: face-lattice(T;eq) free-dist-lattice-with-constraints: free-dist-lattice-with-constraints(T;eq;x.Cs[x]) constrained-antichain-lattice: constrained-antichain-lattice(T;eq;P) mk-bounded-distributive-lattice: mk-bounded-distributive-lattice mk-bounded-lattice: mk-bounded-lattice(T;m;j;z;o) record-update: r[x := v] ifthenelse: if then else fi  eq_atom: =a y bfalse: ff btrue: tt bool: 𝔹 unit: Unit it: uiff: uiff(P;Q) exists: x:A. B[x] sq_type: SQType(T) bnot: ¬bb assert: b false: False not: ¬A squash: T true: True
Lemmas referenced :  cubical-term-equal context-subset_wf context-subset-subtype face-or_wf face-and_wf face-or-eq-1 face-and-eq-1 cubical-term-at_wf face-type_wf lattice-point_wf face_lattice_wf subtype_rel_set bounded-lattice-structure_wf lattice-structure_wf lattice-axioms_wf bounded-lattice-structure-subtype bounded-lattice-axioms_wf equal_wf lattice-meet_wf lattice-join_wf lattice-1_wf I_cube_wf fset_wf nat_wf same-cubical-term_wf cubical-type-cumulativity2 subset-cubical-term2 face-term-implies-subset face-term-and-implies1 face-term-and-implies2 context-subset-subtype-or2 cubical-term_wf context-subset-subtype-or cubical_set_cumulativity-i-j cubical-type_wf cubical_set_wf I_cube_pair_redex_lemma fl-eq_wf subtype_rel_self eqtt_to_assert assert-fl-eq subset-cubical-term context-subset-is-subset eqff_to_assert bool_cases_sqequal subtype_base_sq bool_wf bool_subtype_base assert-bnot iff_weakening_uiff assert_wf subset-cubical-type face-term-implies-or2 face-and-at iff_weakening_equal lattice-meet-idempotent bdd-distributive-lattice-subtype-lattice squash_wf true_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt equalitySymmetry cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis because_Cache equalityTransitivity independent_isectElimination universeIsType applyEquality lambdaFormation_alt dependent_functionElimination productElimination independent_functionElimination inlFormation_alt equalityIstype inhabitedIsType sqequalRule instantiate lambdaEquality_alt productEquality cumulativity isectEquality functionExtensionality Error :memTop,  setElimination rename unionElimination equalityElimination dependent_pairFormation_alt promote_hyp voidElimination dependent_set_memberEquality_alt imageElimination natural_numberEquality imageMemberEquality baseClosed

Latex:
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[phi,psi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[A:\{Gamma,  (phi  \mvee{}  psi)  \mvdash{}  \_\}].  \mforall{}[u:\{Gamma,  phi  \mvdash{}  \_:A\}].
\mforall{}[v:\{Gamma,  psi  \mvdash{}  \_:A\}].
    Gamma,  psi  \mvdash{}  (u  \mvee{}  v)=v:A  supposing  Gamma,  (phi  \mwedge{}  psi)  \mvdash{}  u=v:A



Date html generated: 2020_05_20-PM-03_11_54
Last ObjectModification: 2020_04_07-PM-03_11_49

Theory : cubical!type!theory


Home Index