Step
*
of Lemma
compat-append2
∀[T:Type]. ∀as,cs,bs,ds:T List. (as @ bs || cs @ ds
⇒ bs || ds supposing as = cs ∈ (T List))
BY
{ InductionOnList }
1
1. [T] : Type
⊢ ∀cs,bs,ds:T List. ([] @ bs || cs @ ds
⇒ bs || ds supposing [] = cs ∈ (T List))
2
1. [T] : Type
2. u : T
3. v : T List
4. ∀cs,bs,ds:T List. (v @ bs || cs @ ds
⇒ bs || ds supposing v = cs ∈ (T List))
⊢ ∀cs,bs,ds:T List. ([u / v] @ bs || cs @ ds
⇒ bs || ds supposing [u / v] = cs ∈ (T List))
Latex:
Latex:
\mforall{}[T:Type]. \mforall{}as,cs,bs,ds:T List. (as @ bs || cs @ ds {}\mRightarrow{} bs || ds supposing as = cs)
By
Latex:
InductionOnList
Home
Index