---

Step * of Lemma assert-pair-blex

∀[A,B:Type].
  ∀eq:EqDecider(A). ∀Ra:A ⟶ A ⟶ 𝔹. ∀Rb:B ⟶ B ⟶ 𝔹. ∀x,y:A × B.
    (↑(pair-blex(eq;Ra;Rb) x y) ⇐⇒ pair-lex(A;λa,a'. (↑(Ra a a'));λb,b'. (↑(Rb b b'))) x y)
BY
{ ((UnivCD THENA Auto)
   THEN D -2
   THEN D -1
   THEN RepUR ``pair-blex pair-lex`` 0
   THEN Subst ⌜eq x1 y1 ~ eqof(eq) x1 y1⌝ 0⋅
   THEN Try (Complete ((RepUR ``eqof`` 0 THEN Auto)))
   THEN (RW assert_pushdownC 0 THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].
    \mforall{}eq:EqDecider(A).  \mforall{}Ra:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbB{}.  \mforall{}Rb:B  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbB{}.  \mforall{}x,y:A  \mtimes{}  B.
        (\muparrow{}(pair-blex(eq;Ra;Rb)  x  y)  \mLeftarrow{}{}\mRightarrow{}  pair-lex(A;\mlambda{}a,a'.  (\muparrow{}(Ra  a  a'));\mlambda{}b,b'.  (\muparrow{}(Rb  b  b')))  x  y)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  D  -2
  THEN  D  -1
  THEN  RepUR  ``pair-blex  pair-lex``  0
  THEN  Subst  \mkleeneopen{}eq  x1  y1  \msim{}  eqof(eq)  x1  y1\mkleeneclose{}  0\mcdot{}
  THEN  Try  (Complete  ((RepUR  ``eqof``  0  THEN  Auto)))
  THEN  (RW  assert\_pushdownC  0  THEN  Auto)\mcdot{})

---

Home Index