Nuprl Rule : dependent_pairFormation

Nuprl Rule : dependent_pairFormation_alt

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

H  ⊢ x:A × B ext <a, b>

  BY dependent_pairFormation_alt a y ()

  H  ⊢ a = a ∈ A
  H  ⊢ B[a/x] ext b
  H y:A ⊢ istype(B[y/x])

Latex:
H \mvdash{} x:A \mtimes{} B ext <a, b> BY dependent\_pairFormation\_alt a y () H \mvdash{} a = a H \mvdash{} B[a/x] ext b H y:A \mvdash{} istype(B[y/x]) Date html generated: 2019_06_20-PM-04_11_52 Last ObjectModification: 2018_09_25-PM-02_13_19 Theory : rules Home Index