Nuprl Rule : inrEquality_alt

This rule proved as lemma rule_inr_equality_true in file rules/rules_union.v at https://github.com/vrahli/NuprlInCoq  
H  ⊢ (inr b1 ) = (inr b2 ) ∈ (A + B)

  BY inrEquality_alt ()
  
  H  ⊢ b1 = b2 ∈ B
  H  ⊢ istype(A)

Latex:
H    \mvdash{}  (inr  b1  )  =  (inr  b2  )

    BY  inrEquality\_alt  ()
   
    H    \mvdash{}  b1  =  b2
    H    \mvdash{}  istype(A)


Date html generated: 2019_06_20-PM-04_11_54
Last ObjectModification: 2018_09_25-PM-02_16_36

Theory : rules


Home Index