---

Step * of Lemma base-equal-partial

∀[A:Type]
  ∀[a,b:Base].
    a = b ∈ partial(A) supposing (((a)↓ ⇐⇒ (b)↓) ∧ a = b ∈ A supposing (a)↓) ∧ (¬is-exception(a)) ∧ (¬is-exception(b)) 
  supposing value-type(A)
BY
{ (RepeatFor 4 ((UD THENA Auto)) THEN (At ⌜Type⌝ (D 0)⋅ THENA (InstLemma `equal-wf-base` [⌜A⌝;⌜a⌝;⌜b⌝]⋅ THEN Auto))) }

1
1. A : Type
2. value-type(A)
3. a : Base
4. b : Base
5. (((a)↓ ⇐⇒ (b)↓) ∧ a = b ∈ A supposing (a)↓) ∧ (¬is-exception(a)) ∧ (¬is-exception(b))
⊢ a = b ∈ partial(A)

---

Latex:

---

Latex:
\mforall{}[A:Type]
    \mforall{}[a,b:Base].
        a  =  b 
        supposing  (((a)\mdownarrow{}  \mLeftarrow{}{}\mRightarrow{}  (b)\mdownarrow{})  \mwedge{}  a  =  b  supposing  (a)\mdownarrow{})  \mwedge{}  (\mneg{}is-exception(a))  \mwedge{}  (\mneg{}is-exception(b)) 
    supposing  value-type(A)


By

---

Latex:
(RepeatFor  4  ((UD  THENA  Auto))
  THEN  (At  \mkleeneopen{}Type\mkleeneclose{}  (D  0)\mcdot{}  THENA  (InstLemma  `equal-wf-base`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THEN  Auto))
  )

---

Home Index