---

Step * of Lemma list_pr_length_ind

∀T:Type. ∀Q:(T List) ⟶ (T List) ⟶ ℙ.
  ((∀ps,qs:T List.  ((∀us,vs:T List.  (||us|| + ||vs|| < ||ps|| + ||qs|| ⇒ Q[us;vs])) ⇒ Q[ps;qs]))
  ⇒ {∀ps,qs:T List.  Q[ps;qs]})
BY
{ ((UnivCD) THENA Auto) }

1
1. T : Type
2. Q : (T List) ⟶ (T List) ⟶ ℙ
3. ∀ps,qs:T List.  ((∀us,vs:T List.  (||us|| + ||vs|| < ||ps|| + ||qs|| ⇒ Q[us;vs])) ⇒ Q[ps;qs])
⊢ ∀ps,qs:T List.  Q[ps;qs]

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}Q:(T  List)  {}\mrightarrow{}  (T  List)  {}\mrightarrow{}  \mBbbP{}.
    ((\mforall{}ps,qs:T  List.    ((\mforall{}us,vs:T  List.    (||us||  +  ||vs||  <  ||ps||  +  ||qs||  {}\mRightarrow{}  Q[us;vs]))  {}\mRightarrow{}  Q[ps;qs]))
    {}\mRightarrow{}  \{\mforall{}ps,qs:T  List.    Q[ps;qs]\})


By

---

Latex:
((UnivCD)  THENA  Auto)

---

Home Index