Nuprl Rule : applyEquality

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

H  ⊢ (f1 a1) (f2 a2) ∈ B[a1/x]

  BY applyEquality x:A ⟶ B
  
  H  ⊢ f1 f2 ∈ (x:A ⟶ B)
  H  ⊢ a1 a2 ∈ A



Definitions occuring in rule :  apply: a function: x:A ⟶ B[x] equal: t ∈ T axiom: Ax

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

    BY  applyEquality  x:A  {}\mrightarrow{}  B
   
    H    \mvdash{}  f1  =  f2
    H    \mvdash{}  a1  =  a2



Date html generated: 2016_12_14-AM-08_53_26
Last ObjectModification: 2016_07_08-PM-03_49_08

Theory : rules


Home Index