---

Step * of Lemma fset-closure-unique

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[r:T ⟶ ℕ]. ∀[fs:(T ⟶ T) List]. ∀[s,c1,c2:fset(T)].
  (c1 = c2 ∈ fset(T)) supposing ((c2 = fs closure of s) and (c1 = fs closure of s))
BY
{ (Auto THEN Using [`eq',⌜eq⌝] (BLemma `f-subset_antisymmetry`)⋅ THEN Auto THEN RepeatFor 2 (BackThruSomeHyp')) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[r:T  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[fs:(T  {}\mrightarrow{}  T)  List].  \mforall{}[s,c1,c2:fset(T)].
    (c1  =  c2)  supposing  ((c2  =  fs  closure  of  s)  and  (c1  =  fs  closure  of  s))


By

---

Latex:
(Auto
  THEN  Using  [`eq',\mkleeneopen{}eq\mkleeneclose{}]  (BLemma  `f-subset\_antisymmetry`)\mcdot{}
  THEN  Auto
  THEN  RepeatFor  2  (BackThruSomeHyp'))

---

Home Index