---

Step * of Lemma agree_on_common_append

No Annotations
∀[T:Type]
  ∀as,bs,cs,ds:T List.
    (agree_on_common(T;as;cs) ⇒ agree_on_common(T;bs;ds) ⇒ agree_on_common(T;as @ bs;cs @ ds)) supposing 
       ((∀x∈as.¬(x ∈ ds)) and 
       (∀x∈cs.¬(x ∈ bs)))
BY
{ (InductionOnList THEN Reduce 0) }

1
1. [T] : Type
⊢ ∀bs,cs,ds:T List.
    (agree_on_common(T;[];cs) ⇒ agree_on_common(T;bs;ds) ⇒ agree_on_common(T;bs;cs @ ds)) supposing 
       ((∀x∈[].¬(x ∈ ds)) and 
       (∀x∈cs.¬(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)))
⊢ ∀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)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type]
    \mforall{}as,bs,cs,ds:T  List.
        (agree\_on\_common(T;as;cs)
              {}\mRightarrow{}  agree\_on\_common(T;bs;ds)
              {}\mRightarrow{}  agree\_on\_common(T;as  @  bs;cs  @  ds))  supposing 
              ((\mforall{}x\mmember{}as.\mneg{}(x  \mmember{}  ds))  and 
              (\mforall{}x\mmember{}cs.\mneg{}(x  \mmember{}  bs)))


By

---

Latex:
(InductionOnList  THEN  Reduce  0)

---

Home Index