Nuprl Rule : dependent_set_memberFormation

Nuprl Rule : dependent_set_memberFormation_alt

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

H  ⊢ {x:A| B}  ext a

  BY dependent_set_memberFormation_alt a y ()

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

Latex:
H \mvdash{} \{x:A| B\} ext a BY dependent\_set\_memberFormation\_alt a y () H \mvdash{} a = a H \mvdash{} B[a/x] H y:A \mvdash{} istype(B[y/x]) Date html generated: 2019_06_20-PM-04_11_59 Last ObjectModification: 2018_09_25-PM-02_46_55 Theory : rules Home Index