---

Step * of Lemma decidable__llex-le

∀[A:Type]. ∀[<:A ⟶ A ⟶ ℙ].
  ((∀a,b:A.  (Dec(<[a;b]) ∧ Dec(a = b ∈ A))) ⇒ (∀L1,L2:A List.  Dec(L1 llex-le(A;a,b.<[a;b]) L2)))
BY
{ (InstLemma `decidable__llex` [] THEN RepeatFor 5 ((ParallelLast' THENA Auto))) }

1
1. [A] : Type
2. [<] : A ⟶ A ⟶ ℙ
3. ∀a,b:A.  (Dec(<[a;b]) ∧ Dec(a = b ∈ A))
4. L1 : A List
5. L2 : A List
6. Dec(L1 llex(A;a,b.<[a;b]) L2)
⊢ Dec(L1 llex-le(A;a,b.<[a;b]) L2)

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[<:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}a,b:A.    (Dec(<[a;b])  \mwedge{}  Dec(a  =  b)))  {}\mRightarrow{}  (\mforall{}L1,L2:A  List.    Dec(L1  llex-le(A;a,b.<[a;b])  L2)))


By

---

Latex:
(InstLemma  `decidable\_\_llex`  []  THEN  RepeatFor  5  ((ParallelLast'  THENA  Auto)))

---

Home Index