Nuprl Lemma : per-or-equal
∀[A1,B1,A2,B2:Type]. (per-or(A1;B1) = per-or(A2;B2) ∈ Type) supposing (A1 ≡ A2 and B1 ≡ B2)
Proof
Definitions occuring in Statement :
per-or: per-or(A;B),
ext-eq: A ≡ B,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
per-or: per-or(A;B),
per-exists: per-exists(A;a.B[a]),
per-product: per-product(A;a.B[a]),
uand: uand(A;B),
has-value: (a)↓,
top: Top,
prop: ℙ,
guard: {T},
implies: P ⇒ Q,
all: ∀x:A. B[x],
sq_type: SQType(T),
subtype_rel: A ⊆r B
Lemmas referenced :
has-value_wf_base,
is-exception_wf,
istype-top,
istype-void,
ext-eq_wf,
uand_wf,
equal-wf-base,
per-value-property,
top_wf,
per-value_subtype_base,
per-value_wf,
subtype_base_sq,
subtype_rel_weakening,
ext-eq_inversion,
equal_functionality_wrt_subtype_rel2,
istype-universe
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :isect_memberFormation_alt,
introduction,
cut,
pertypeEquality,
sqequalHypSubstitution,
isectElimination,
thin,
baseClosed,
sqequalRule,
axiomSqleEquality,
divergentSqle,
sqleReflexivity,
extract_by_obid,
hypothesis,
rename,
isaxiomCases,
hypothesisEquality,
axiomSqEquality,
because_Cache,
Error :inhabitedIsType,
Error :isect_memberEquality_alt,
voidElimination,
independent_isectElimination,
axiomEquality,
Error :universeIsType,
equalitySymmetry,
promote_hyp,
equalityTransitivity,
universeEquality,
sqequalIntensionalEquality,
baseApply,
closedConclusion,
isectEquality,
isect_memberFormation,
isect_memberEquality,
voidEquality,
independent_functionElimination,
dependent_functionElimination,
cumulativity,
instantiate,
applyEquality,
Error :lambdaFormation_alt,
Error :equalityIsType4
Latex:
\mforall{}[A1,B1,A2,B2:Type]. (per-or(A1;B1) = per-or(A2;B2)) supposing (A1 \mequiv{} A2 and B1 \mequiv{} B2)
Date html generated:
2019_06_20-AM-11_30_35
Last ObjectModification:
2018_10_06-AM-10_00_52
Theory : per!type
Home
Index