---

Step * 2 of Lemma agree_on_common_append


1. [T] : Type
2. u : T
3. v : T List
4. ∀bs,cs,ds:T List.
     (agree_on_common(T;v;cs) ⇒ agree_on_common(T;bs;ds) ⇒ agree_on_common(T;v @ bs;cs @ ds)) supposing 
        ((∀x∈v.¬(x ∈ ds)) and 
        (∀x∈cs.¬(x ∈ bs)))
⊢ ∀bs,cs,ds:T List.
    (agree_on_common(T;[u / v];cs) ⇒ agree_on_common(T;bs;ds) ⇒ agree_on_common(T;[u / (v @ bs)];cs @ ds)) supposing 
       ((∀x∈[u / v].¬(x ∈ ds)) and 
       (∀x∈cs.¬(x ∈ bs)))
BY
{ ((D 0 THENA Auto) THEN InductionOnList) }

1
1. [T] : Type
2. u : T
3. v : T List
4. ∀bs,cs,ds:T List.
     (agree_on_common(T;v;cs) ⇒ agree_on_common(T;bs;ds) ⇒ agree_on_common(T;v @ bs;cs @ ds)) supposing 
        ((∀x∈v.¬(x ∈ ds)) and 
        (∀x∈cs.¬(x ∈ bs)))
5. bs : T List
⊢ ∀ds:T List
    (agree_on_common(T;[u / v];[]) ⇒ agree_on_common(T;bs;ds) ⇒ agree_on_common(T;[u / (v @ bs)];[] @ ds)) supposing 
       ((∀x∈[u / v].¬(x ∈ ds)) and 
       (∀x∈[].¬(x ∈ bs)))

2
1. [T] : Type
2. u : T
3. v : T List
4. ∀bs,cs,ds:T List.
     (agree_on_common(T;v;cs) ⇒ agree_on_common(T;bs;ds) ⇒ agree_on_common(T;v @ bs;cs @ ds)) supposing 
        ((∀x∈v.¬(x ∈ ds)) and 
        (∀x∈cs.¬(x ∈ bs)))
5. bs : T List
6. u1 : T
7. v1 : T List
8. ∀ds:T List
     (agree_on_common(T;[u / v];v1) ⇒ agree_on_common(T;bs;ds) ⇒ agree_on_common(T;[u / (v @ bs)];v1 @ ds)) supposing 
        ((∀x∈[u / v].¬(x ∈ ds)) and 
        (∀x∈v1.¬(x ∈ bs)))
⊢ ∀ds:T List
    (agree_on_common(T;[u / v];[u1 / v1])
       ⇒ agree_on_common(T;bs;ds)
       ⇒ agree_on_common(T;[u / (v @ bs)];[u1 / v1] @ ds)) supposing 
       ((∀x∈[u / v].¬(x ∈ ds)) and 
       (∀x∈[u1 / v1].¬(x ∈ bs)))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  u  :  T
3.  v  :  T  List
4.  \mforall{}bs,cs,ds:T  List.
          (agree\_on\_common(T;v;cs)
                {}\mRightarrow{}  agree\_on\_common(T;bs;ds)
                {}\mRightarrow{}  agree\_on\_common(T;v  @  bs;cs  @  ds))  supposing 
                ((\mforall{}x\mmember{}v.\mneg{}(x  \mmember{}  ds))  and 
                (\mforall{}x\mmember{}cs.\mneg{}(x  \mmember{}  bs)))
\mvdash{}  \mforall{}bs,cs,ds:T  List.
        (agree\_on\_common(T;[u  /  v];cs)
              {}\mRightarrow{}  agree\_on\_common(T;bs;ds)
              {}\mRightarrow{}  agree\_on\_common(T;[u  /  (v  @  bs)];cs  @  ds))  supposing 
              ((\mforall{}x\mmember{}[u  /  v].\mneg{}(x  \mmember{}  ds))  and 
              (\mforall{}x\mmember{}cs.\mneg{}(x  \mmember{}  bs)))


By

---

Latex:
((D  0  THENA  Auto)  THEN  InductionOnList)

---

Home Index