Nuprl Rule : sqleExtensionalEquality
This rule proved as lemma rule_approx_extensional_equality_true in file rules/rules_squiggle4.v
at https://github.com/vrahli/NuprlInCoq
H ⊢ (a ≤ b) = (c ≤ d) ∈ Type
BY sqleExtensionalEquality ()
H ⊢ ↓a ≤ b ⇐⇒ c ≤ d
Definitions occuring in rule :
equal: s = t ∈ T,
universe: Type,
squash: ↓T,
iff: P ⇐⇒ Q,
sqle: s ≤ t,
axiom: Ax
Latex:
H \mvdash{} (a \mleq{} b) = (c \mleq{} d)
BY sqleExtensionalEquality ()
H \mvdash{} \mdownarrow{}a \mleq{} b \mLeftarrow{}{}\mRightarrow{} c \mleq{} d
Date html generated:
2019_06_20-PM-04_12_16
Last ObjectModification:
2016_07_08-PM-03_48_46
Theory : rules
Home
Index