Nuprl Rule : equalityEqualityBase
This rule proved as lemma rule_equality_equality_base_or_true in file rules/rules_equality.v
at https://github.com/vrahli/NuprlInCoq
H ⊢ (a11 = a12 ∈ A1) = (a21 = a22 ∈ A2) ∈ Type
BY equalityEqualityBase x p ()
H ⊢ A1 = A2 ∈ Type
H ⊢ a11 = a21 ∈ Image((x:ℤ + ℤ × case x of inl() => A1 | inr() => Base),(λp.(snd(p))))
H ⊢ a12 = a22 ∈ Image((x:ℤ + ℤ × case x of inl() => A1 | inr() => Base),(λp.(snd(p))))
Definitions occuring in rule :
universe: Type,
equal: s = t ∈ T,
image-type: Image(T,f),
product: x:A × B[x],
union: left + right,
int: ℤ,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
base: Base,
lambda: λx.A[x],
pi2: snd(t),
axiom: Ax
Latex:
H \mvdash{} (a11 = a12) = (a21 = a22)
BY equalityEqualityBase x p ()
H \mvdash{} A1 = A2
H \mvdash{} a11 = a21
H \mvdash{} a12 = a22
Date html generated:
2017_09_29-PM-05_45_14
Last ObjectModification:
2017_02_24-PM-04_22_33
Theory : rules
Home
Index