### 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