Nuprl Rule : pointwiseFunctionality
This rule proved as lemma rule_functionaliy_true in file rules/rules_functionality.v
at https://github.com/vrahli/NuprlInCoq
H z:A, J ⊢ C ext t
BY pointwiseFunctionality #$i !parameter{j:l} a b c ()
H [a:Base], [b:Base], [c:(a = b ∈ A)], J[a/z] ⊢ C[a/z] ext t
H a:Base, b:Base, c:(a = b ∈ A), J[a/z] ⊢ C[a/z] = C[b/z] ∈ 𝕌{j}
Definitions occuring in rule :
base: Base,
equal: s = t ∈ T,
universe: Type,
axiom: Ax
Latex:
H z:A, J \mvdash{} C ext t
BY pointwiseFunctionality \#\$i !parameter\{j:l\} a b c ()
H [a:Base], [b:Base], [c:(a = b)], J[a/z] \mvdash{} C[a/z] ext t
H a:Base, b:Base, c:(a = b), J[a/z] \mvdash{} C[a/z] = C[b/z]
Date html generated:
2019_06_20-PM-04_11_54
Last ObjectModification:
2016_07_08-PM-03_48_49
Theory : rules
Home
Index