---

Step * of Lemma member-insert-by

∀[T:Type]
  ∀eq,r:T ⟶ T ⟶ 𝔹.
    ∀x:T. ∀L:T List. ∀z:T.  ((z ∈ insert-by(eq;r;x;L)) ⇐⇒ (z = x ∈ T) ∨ (z ∈ L)) 
    supposing ∀a,b:T.  (↑(eq a b) ⇐⇒ a = b ∈ T)
BY
{ (((InductionOnList THEN Unfold `insert-by` 0 THEN Reduce 0 THEN Try (Fold `insert-by` 0) THEN UnivCD) THENA Auto)
   THEN ((((Repeat ((SplitOnConclITE THENA Auto)) THEN RWW "member_singleton" 0) THENA Auto) THEN RWW "cons_member" 0)
         THENA Auto
         )
   THEN RWW "nil_member" 0
   THEN Auto
   THEN SplitOrHyps
   THEN Auto
   THEN Try (Complete (((OrRight THENM BackThruSomeHyp) THEN Auto)))
   THEN ∀h:hyp. (((InstHyp [⌜z⌝] h)⋅ THENA Complete (Auto)) THEN ThinTrivial) 
   THEN SplitOrHyps
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}eq,r:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}.
        \mforall{}x:T.  \mforall{}L:T  List.  \mforall{}z:T.    ((z  \mmember{}  insert-by(eq;r;x;L))  \mLeftarrow{}{}\mRightarrow{}  (z  =  x)  \mvee{}  (z  \mmember{}  L)) 
        supposing  \mforall{}a,b:T.    (\muparrow{}(eq  a  b)  \mLeftarrow{}{}\mRightarrow{}  a  =  b)


By

---

Latex:
(((InductionOnList
      THEN  Unfold  `insert-by`  0
      THEN  Reduce  0
      THEN  Try  (Fold  `insert-by`  0)
      THEN  UnivCD)
    THENA  Auto
    )
  THEN  ((((Repeat  ((SplitOnConclITE  THENA  Auto))  THEN  RWW  "member\_singleton"  0)  THENA  Auto)
                THEN  RWW  "cons\_member"  0
                )
              THENA  Auto
              )
  THEN  RWW  "nil\_member"  0
  THEN  Auto
  THEN  SplitOrHyps
  THEN  Auto
  THEN  Try  (Complete  (((OrRight  THENM  BackThruSomeHyp)  THEN  Auto)))
  THEN  \mforall{}h:hyp.  (((InstHyp  [\mkleeneopen{}z\mkleeneclose{}]  h)\mcdot{}  THENA  Complete  (Auto))  THEN  ThinTrivial) 
  THEN  SplitOrHyps
  THEN  Auto)

---

Home Index