Nuprl Rule : isectEquality

This rule proved as lemma rule_isect_equality_true3 in file rules/rules_isect.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ (⋂x1:a1. b1) = (⋂x2:a2. b2) ∈ Type

  BY isectEquality y ()

  H  ⊢ a1 = a2 ∈ Type
  H y:a1 ⊢ b1[y/x1] = b2[y/x2] ∈ Type

Definitions occuring in rule : isect: ⋂x:A. B[x], equal: s = t ∈ T, universe: Type, axiom: Ax

Latex:
H \mvdash{} (\mcap{}x1:a1. b1) = (\mcap{}x2:a2. b2) BY isectEquality y () H \mvdash{} a1 = a2 H y:a1 \mvdash{} b1[y/x1] = b2[y/x2] Date html generated: 2019_06_20-PM-04_11_52 Last ObjectModification: 2016_07_08-PM-03_48_54 Theory : rules Home Index