---

Step * of Lemma sq_stable__bs_tree_ordered

∀[E:Type]. ∀cmp:comparison(E). ∀tr:bs_tree(E).  SqStable(bs_tree_ordered(E;cmp;tr))
BY
{ (RepeatFor 2 (Intro)
   THEN BLemma `bs_tree-induction`
   THEN Auto
   THEN RepUR ``bs_tree_ordered`` 0
   THEN Try (Fold `bs_tree_ordered` 0)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[E:Type].  \mforall{}cmp:comparison(E).  \mforall{}tr:bs\_tree(E).    SqStable(bs\_tree\_ordered(E;cmp;tr))


By

---

Latex:
(RepeatFor  2  (Intro)
  THEN  BLemma  `bs\_tree-induction`
  THEN  Auto
  THEN  RepUR  ``bs\_tree\_ordered``  0
  THEN  Try  (Fold  `bs\_tree\_ordered`  0)
  THEN  Auto)

---

Home Index