---

Step * 1 of Lemma DCC-order-type-less


1. f : ℕ ⟶ (A:Type × <:A ⟶ A ⟶ ℙ × DCC(A;<))
2. ∀i:ℕ. ((f (i + 1)) order-type-less() (f i))
⊢ False
BY
{ ((Assert ∀i:ℕ
             ∃f@0:(fst((f (i + 1)))) ⟶ (fst((f i)))
              ∃b:fst((f i))
               (order-preserving(fst((f (i + 1)));fst((f i));a1,a2.a1 (fst(snd((f (i + 1))))) a2;b1,b2.b1 
                                                                                                       (fst(snd((f 
                                                                                                                 i)))) 
                                                                                                       b2;f@0)
               ∧ (∀a:fst((f (i + 1))). ((f@0 a) (fst(snd((f i)))) b))) BY
          (ParallelLast
           THEN MoveToConcl (-1)
           THEN GenConclTerms Auto [⌜f (i + 1)⌝;⌜f i⌝]⋅
           THEN RepeatFor 2 (D -4)
           THEN RepeatFor 2 (D -2)
           THEN RepUR ``order-type-less`` 0
           THEN Auto))
   THEN Thin (-2)
   ) }

1
1. f : ℕ ⟶ (A:Type × <:A ⟶ A ⟶ ℙ × DCC(A;<))
2. ∀i:ℕ
     ∃f@0:(fst((f (i + 1)))) ⟶ (fst((f i)))
      ∃b:fst((f i))
       (order-preserving(fst((f (i + 1)));fst((f 
                                               i));a1,a2.a1 (fst(snd((f (i + 1))))) a2;b1,b2.b1 
                                                                                             (fst(snd((f i)))) 
                                                                                             b2;f@0)
       ∧ (∀a:fst((f (i + 1))). ((f@0 a) (fst(snd((f i)))) b)))
⊢ False

---

Latex:

---

Latex:

1.  f  :  \mBbbN{}  {}\mrightarrow{}  (A:Type  \mtimes{}  <:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}  \mtimes{}  DCC(A;<))
2.  \mforall{}i:\mBbbN{}.  ((f  (i  +  1))  order-type-less()  (f  i))
\mvdash{}  False


By

---

Latex:
((Assert  \mforall{}i:\mBbbN{}
                      \mexists{}f@0:(fst((f  (i  +  1))))  {}\mrightarrow{}  (fst((f  i)))
                        \mexists{}b:fst((f  i))
                          (order-preserving(fst((f  (i  +  1)));fst((f 
                                                                                                          i));a1,a2.a1 
                                                                                                                              (fst(snd((f  (i  +  1))))) 
                                                                                                                              a2;b1,b2.b1  (fst(snd((f  i))))  b2;f@0)
                          \mwedge{}  (\mforall{}a:fst((f  (i  +  1))).  ((f@0  a)  (fst(snd((f  i))))  b)))  BY
                (ParallelLast
                  THEN  MoveToConcl  (-1)
                  THEN  GenConclTerms  Auto  [\mkleeneopen{}f  (i  +  1)\mkleeneclose{};\mkleeneopen{}f  i\mkleeneclose{}]\mcdot{}
                  THEN  RepeatFor  2  (D  -4)
                  THEN  RepeatFor  2  (D  -2)
                  THEN  RepUR  ``order-type-less``  0
                  THEN  Auto))
  THEN  Thin  (-2)
  )

---

Home Index