---

Step * 2 of Lemma insert-int-comm


1. ∀L:ℤ List. ∀a,b:ℤ.  (insert-int(b;insert-int(a;L)) = insert-int(a;insert-int(b;L)) ∈ (ℤ List))
⊢ ∀T:Type. ∀a,b:T.
    ((T ⊆r ℤ) ⇒ (∀L:T List. (insert-int(b;insert-int(a;L)) = insert-int(a;insert-int(b;L)) ∈ (T List))))
BY
{ (Intros THEN (InstHyp [⌜L⌝;⌜a⌝;⌜b⌝] 1⋅ THENA Auto) THEN HypSubst' (-1) 0 THEN Fold `member` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  \mforall{}L:\mBbbZ{}  List.  \mforall{}a,b:\mBbbZ{}.    (insert-int(b;insert-int(a;L))  =  insert-int(a;insert-int(b;L)))
\mvdash{}  \mforall{}T:Type.  \mforall{}a,b:T.
        ((T  \msubseteq{}r  \mBbbZ{})  {}\mRightarrow{}  (\mforall{}L:T  List.  (insert-int(b;insert-int(a;L))  =  insert-int(a;insert-int(b;L)))))


By

---

Latex:
(Intros
  THEN  (InstHyp  [\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]  1\mcdot{}  THENA  Auto)
  THEN  HypSubst'  (-1)  0
  THEN  Fold  `member`  0
  THEN  Auto)

---

Home Index