---

Step * of Lemma sq_stable__l_subset

∀[T:Type]. ∀[L1:T List].  ∀L2:T List. ((∀x,y:T.  Dec(x = y ∈ T)) ⇒ SqStable(l_subset(T;L1;L2)))
BY
{ (Auto
   THEN RepUR ``sq_stable l_subset`` 0
   THEN Auto
   THEN (InstLemma `decidable__l_member` [⌜T⌝;⌜x⌝;⌜L2⌝]⋅ THENA Auto)
   THEN D (-1)
   THEN Auto
   THEN Assert ⌜False⌝⋅
   THEN Auto
   THEN (D (-4) THENA Auto)
   THEN FHyp (-4) [-2]
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L1:T  List].    \mforall{}L2:T  List.  ((\mforall{}x,y:T.    Dec(x  =  y))  {}\mRightarrow{}  SqStable(l\_subset(T;L1;L2)))


By

---

Latex:
(Auto
  THEN  RepUR  ``sq\_stable  l\_subset``  0
  THEN  Auto
  THEN  (InstLemma  `decidable\_\_l\_member`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}L2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  (-1)
  THEN  Auto
  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  (D  (-4)  THENA  Auto)
  THEN  FHyp  (-4)  [-2]
  THEN  Auto)

---

Home Index