---

Step * of Lemma pair-lex_well_fnd

∀[A,B:Type]. ∀[Ra:A ⟶ A ⟶ ℙ]. ∀[Rb:B ⟶ B ⟶ ℙ].
  (WellFnd{i}(A;a1,a2.Ra a1 a2) ⇒ WellFnd{i}(B;b1,b2.Rb b1 b2) ⇒ WellFnd{i}(A × B;p1,p2.pair-lex(A;Ra;Rb) p1 p2))
BY
{ (InstLemma `product_well_fnd` []
   THEN RepeatFor 4 (ParallelLast')
   THEN Unfold `so_apply` (-1)
   THEN Auto
   THEN RepeatFor 2 (ThinTrivial)
   THEN RepeatFor 7 (ParallelLast)
   THEN (D  (-3) THEN D -2)
   THEN RepUR ``pair-lex`` -1
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[Ra:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[Rb:B  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}].
    (WellFnd\{i\}(A;a1,a2.Ra  a1  a2)
    {}\mRightarrow{}  WellFnd\{i\}(B;b1,b2.Rb  b1  b2)
    {}\mRightarrow{}  WellFnd\{i\}(A  \mtimes{}  B;p1,p2.pair-lex(A;Ra;Rb)  p1  p2))


By

---

Latex:
(InstLemma  `product\_well\_fnd`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  Unfold  `so\_apply`  (-1)
  THEN  Auto
  THEN  RepeatFor  2  (ThinTrivial)
  THEN  RepeatFor  7  (ParallelLast)
  THEN  (D    (-3)  THEN  D  -2)
  THEN  RepUR  ``pair-lex``  -1
  THEN  Reduce  0
  THEN  Auto)

---

Home Index