Nuprl Rule : pointwiseFunctionalityForEquality
This rule proved as lemma rule_functionaliy_for_equality_true in file rules/rules_functionality.v
at https://github.com/vrahli/NuprlInCoq
H a:A, J ⊢ t1 = t2 ∈ T
BY pointwiseFunctionalityForEquality #$i !parameter{j:l} b z ()
H a:A, J ⊢ T ∈ 𝕌{j}
H a:Base, b:Base, z:(a = b ∈ A), J ⊢ t1 = t2[b/a] ∈ T
Definitions occuring in rule :
member: t ∈ T,
universe: Type,
base: Base,
equal: s = t ∈ T,
axiom: Ax
Latex:
H a:A, J \mvdash{} t1 = t2
BY pointwiseFunctionalityForEquality \#\$i !parameter\{j:l\} b z ()
H a:A, J \mvdash{} T \mmember{} \mBbbU{}\{j\}
H a:Base, b:Base, z:(a = b), J \mvdash{} t1 = t2[b/a]
Date html generated:
2019_06_20-PM-04_12_02
Last ObjectModification:
2017_02_24-PM-02_37_55
Theory : rules
Home
Index