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 ()
  
  H  ⊢ a ∈ A
  H  ⊢ B[a/x]
  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