---

Step * of Lemma no_repeats-before-equality

∀[T:Type]
  ∀as,bs:T List.
    (as = bs ∈ (T List)
       ⇐⇒ (∀x:T. ((x ∈ as) ⇐⇒ (x ∈ bs))) ∧ (∀x,y:T.  (x before y ∈ as ⇐⇒ x before y ∈ bs))) supposing 
       (no_repeats(T;bs) and 
       no_repeats(T;as))
BY
{ xxx(Auto
      THEN Try ((Subst ⌜as = bs ∈ (T List)⌝ 0⋅ THEN Complete (Auto)))
      THEN Try ((Subst ⌜bs = as ∈ (T List)⌝ 0⋅ THEN Complete (Auto))))xxx }

1
1. T : Type
2. as : T List
3. bs : T List
4. no_repeats(T;as)
5. no_repeats(T;bs)
6. ∀x:T. ((x ∈ as) ⇐⇒ (x ∈ bs))
7. ∀x,y:T.  (x before y ∈ as ⇐⇒ x before y ∈ bs)
⊢ as = bs ∈ (T List)

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}as,bs:T  List.
        (as  =  bs
              \mLeftarrow{}{}\mRightarrow{}  (\mforall{}x:T.  ((x  \mmember{}  as)  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  bs)))
                      \mwedge{}  (\mforall{}x,y:T.    (x  before  y  \mmember{}  as  \mLeftarrow{}{}\mRightarrow{}  x  before  y  \mmember{}  bs)))  supposing 
              (no\_repeats(T;bs)  and 
              no\_repeats(T;as))


By

---

Latex:
xxx(Auto
        THEN  Try  ((Subst  \mkleeneopen{}as  =  bs\mkleeneclose{}  0\mcdot{}  THEN  Complete  (Auto)))
        THEN  Try  ((Subst  \mkleeneopen{}bs  =  as\mkleeneclose{}  0\mcdot{}  THEN  Complete  (Auto))))xxx

---

Home Index