Nuprl Rule : functionEquality
This rule proved as lemma rule_function_equality_true in file rules/rules_function.v
 at https://github.com/vrahli/NuprlInCoq  
H  ⊢ (x1:a1 ⟶ b1) = (x2:a2 ⟶ b2) ∈ Type
  BY functionEquality y
  
  H  ⊢ a1 = a2 ∈ Type
  H y:a1 ⊢ b1[y/x1] = b2[y/x2] ∈ Type
Definitions occuring in rule : 
function: x:A ⟶ B[x]
, 
equal: s = t ∈ T
, 
universe: Type
, 
axiom: Ax
Latex:
H    \mvdash{}  (x1:a1  {}\mrightarrow{}  b1)  =  (x2:a2  {}\mrightarrow{}  b2)
    BY  functionEquality  y
   
    H    \mvdash{}  a1  =  a2
    H  y:a1  \mvdash{}  b1[y/x1]  =  b2[y/x2]
Date html generated:
2019_06_20-PM-04_11_48
Last ObjectModification:
2016_07_08-PM-03_48_57
Theory : rules
Home
Index