Nuprl Lemma : context-subset-subtype-and2

[Gamma:j⊢]. ∀[phi1,phi2:{Gamma ⊢ _:𝔽}].  ({Gamma, phi2 ⊢ _} ⊆{Gamma, (phi1 ∧ phi2) ⊢ _})


Proof




Definitions occuring in Statement :  context-subset: Gamma, phi face-and: (a ∧ b) face-type: 𝔽 cubical-term: {X ⊢ _:A} cubical-type: {X ⊢ _} cubical_set: CubicalSet subtype_rel: A ⊆B uall: [x:A]. B[x]
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a subtype_rel: A ⊆B
Lemmas referenced :  subset-cubical-type context-subset_wf face-and_wf face-term-implies-subset face-term-and-implies2 cubical-term_wf face-type_wf cubical_set_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis independent_isectElimination instantiate because_Cache sqequalRule axiomEquality inhabitedIsType isect_memberEquality_alt isectIsTypeImplies universeIsType

Latex:
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[phi1,phi2:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].    (\{Gamma,  phi2  \mvdash{}  \_\}  \msubseteq{}r  \{Gamma,  (phi1  \mwedge{}  phi2)  \mvdash{}  \_\})



Date html generated: 2020_05_20-PM-02_52_45
Last ObjectModification: 2020_04_04-PM-05_07_15

Theory : cubical!type!theory


Home Index