Nuprl Rule : spreadEquality
This rule proved as lemma rule_spread_equality_true in file rules/rules_product.v
at https://github.com/vrahli/NuprlInCoq
H ⊢ let x1,y1 = e1 in t1 = let x2,y2 = e2 in t2 ∈ T[e1/z]
BY spreadEquality z.T (w:A × B) u v a ()
H ⊢ e1 = e2 ∈ (w:A × B)
H u:A, v:B[u/w], a:(e1 = <u, v> ∈ (w:A × B)) ⊢ t1[u,v/x1,y1] = t2[u,v/x2,y2] ∈ T[<u, v>/z]
Definitions occuring in rule :
spread: spread def,
product: x:A × B[x],
equal: s = t ∈ T,
pair: <a, b>,
axiom: Ax
Latex:
H \mvdash{} let x1,y1 = e1 in t1 = let x2,y2 = e2 in t2
BY spreadEquality z.T (w:A \mtimes{} B) u v a ()
H \mvdash{} e1 = e2
H u:A, v:B[u/w], a:(e1 = <u, v>) \mvdash{} t1[u,v/x1,y1] = t2[u,v/x2,y2]
Date html generated:
2019_06_20-PM-04_11_53
Last ObjectModification:
2016_07_08-PM-03_48_48
Theory : rules
Home
Index