Nuprl Rule : inlEquality_alt

This rule proved as lemma rule_inl_equality_true in file rules/rules_union.v at https://github.com/vrahli/NuprlInCoq  
H  ⊢ (inl a1) = (inl a2) ∈ (A + B)

  BY inlEquality_alt ()
  
  H  ⊢ a1 = a2 ∈ A
  H  ⊢ istype(B)

Latex:
H    \mvdash{}  (inl  a1)  =  (inl  a2)

    BY  inlEquality\_alt  ()
   
    H    \mvdash{}  a1  =  a2
    H    \mvdash{}  istype(B)


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

Theory : rules


Home Index