Nuprl Rule : imageEquality
This rule proved as lemma rule_image_equality_true in file rules/rules_image.v at https://github.com/vrahli/NuprlInCoq
H ⊢ Image(A1,f1) = Image(A2,f2) ∈ Type
BY imageEquality !parameter{i:l} ()
H ⊢ f1 = f2 ∈ Base
H ⊢ A1 = A2 ∈ Type
Definitions occuring in rule :
image-type: Image(T,f),
base: Base,
equal: s = t ∈ T,
universe: Type,
axiom: Ax
Latex:
H \mvdash{} Image(A1,f1) = Image(A2,f2)
BY imageEquality !parameter\{i:l\} ()
H \mvdash{} f1 = f2
H \mvdash{} A1 = A2
Date html generated:
2019_06_20-PM-04_12_30
Last ObjectModification:
2016_07_08-PM-03_48_57
Theory : rules
Home
Index