---

Step * of Lemma agree_on_common_cons

∀[T:Type]. ∀as,bs:T List. ∀x:T.  (agree_on_common(T;[x / as];[x / bs]) ⇐⇒ agree_on_common(T;as;bs))
BY
{ Auto }

1
1. [T] : Type
2. as : T List
3. bs : T List
4. x : T
5. agree_on_common(T;[x / as];[x / bs])
⊢ agree_on_common(T;as;bs)

2
1. [T] : Type
2. as : T List
3. bs : T List
4. x : T
5. agree_on_common(T;as;bs)
⊢ agree_on_common(T;[x / as];[x / bs])

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}as,bs:T  List.  \mforall{}x:T.    (agree\_on\_common(T;[x  /  as];[x  /  bs])  \mLeftarrow{}{}\mRightarrow{}  agree\_on\_common(T;as;bs))


By

---

Latex:
Auto

---

Home Index