---

Step * 1 1 2 of Lemma agree_on_common_append


1. [T] : Type
2. bs : T List
3. u : T
4. v : T List
5. ∀ds:T List
     (agree_on_common(T;[];v) ⇒ agree_on_common(T;bs;ds) ⇒ agree_on_common(T;bs;v @ ds)) supposing 
        ((∀x∈[].¬(x ∈ ds)) and 
        (∀x∈v.¬(x ∈ bs)))
6. ds : T List
7. (∀x∈[u / v].¬(x ∈ bs))
8. (∀x∈[].¬(x ∈ ds))
9. agree_on_common(T;[];[u / v])
10. agree_on_common(T;bs;ds)
11. agree_on_common(T;bs;v @ ds)
⊢ agree_on_common(T;bs;[u / (v @ ds)])
BY
{ ((((InstLemma `agree_on_common_cons2` [T;bs;v @ ds;u] THENA Auto) THEN D (-1)) THEN D (-1)) THEN EasyHyp) }

1
1. T : Type
2. bs : T List
3. u : T
4. v : T List
5. ∀ds:T List
     (agree_on_common(T;[];v) ⇒ agree_on_common(T;bs;ds) ⇒ agree_on_common(T;bs;v @ ds)) supposing 
        ((∀x∈[].¬(x ∈ ds)) and 
        (∀x∈v.¬(x ∈ bs)))
6. ds : T List
7. (∀x∈[u / v].¬(x ∈ bs))
8. (∀x∈[].¬(x ∈ ds))
9. agree_on_common(T;[];[u / v])
10. agree_on_common(T;bs;ds)
11. agree_on_common(T;bs;v @ ds)
12. agree_on_common(T;[u / bs];v @ ds) ⇐⇒ agree_on_common(T;bs;v @ ds) supposing ¬(u ∈ v @ ds)
⊢ ¬(u ∈ bs)

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  bs  :  T  List
3.  u  :  T
4.  v  :  T  List
5.  \mforall{}ds:T  List
          (agree\_on\_common(T;[];v)
                {}\mRightarrow{}  agree\_on\_common(T;bs;ds)
                {}\mRightarrow{}  agree\_on\_common(T;bs;v  @  ds))  supposing 
                ((\mforall{}x\mmember{}[].\mneg{}(x  \mmember{}  ds))  and 
                (\mforall{}x\mmember{}v.\mneg{}(x  \mmember{}  bs)))
6.  ds  :  T  List
7.  (\mforall{}x\mmember{}[u  /  v].\mneg{}(x  \mmember{}  bs))
8.  (\mforall{}x\mmember{}[].\mneg{}(x  \mmember{}  ds))
9.  agree\_on\_common(T;[];[u  /  v])
10.  agree\_on\_common(T;bs;ds)
11.  agree\_on\_common(T;bs;v  @  ds)
\mvdash{}  agree\_on\_common(T;bs;[u  /  (v  @  ds)])


By

---

Latex:
((((InstLemma  `agree\_on\_common\_cons2`  [T;bs;v  @  ds;u]  THENA  Auto)  THEN  D  (-1))  THEN  D  (-1))
  THEN  EasyHyp
  )

---

Home Index