Nuprl Rule : functionExtensionality_alt

H  ⊢ f = g ∈ (x:A ⟶ B)

  BY functionExtensionality_alt u ()
  
  H u:A ⊢ (f u) = (g u) ∈ B[u/x]
  H  ⊢ istype(A)

Latex:
H    \mvdash{}  f  =  g

    BY  functionExtensionality\_alt  u  ()
   
    H  u:A  \mvdash{}  (f  u)  =  (g  u)
    H    \mvdash{}  istype(A)


Date html generated: 2019_06_20-PM-04_11_56
Last ObjectModification: 2018_09_25-PM-02_17_37

Theory : rules


Home Index