Step * 2 2 of Lemma compat-append2


1. [T] Type
2. T
3. List
4. ∀cs,bs,ds:T List.  (v bs || cs ds  bs || ds supposing cs ∈ (T List))
5. u1 T
6. v1 List
7. ∀bs,ds:T List.  ([u v] bs || v1 ds  bs || ds supposing [u v] v1 ∈ (T List))
⊢ ∀bs,ds:T List.  ([u v] bs || [u1 v1] ds  bs || ds supposing [u v] [u1 v1] ∈ (T List))
BY
Auto ⋅ }

1
1. [T] Type
2. T
3. List
4. ∀cs,bs,ds:T List.  (v bs || cs ds  bs || ds supposing cs ∈ (T List))
5. u1 T
6. v1 List
7. ∀bs,ds:T List.  ([u v] bs || v1 ds  bs || ds supposing [u v] v1 ∈ (T List))
8. bs List
9. ds List
10. [u v] bs || [u1 v1] ds
11. [u v] [u1 v1] ∈ (T List)
⊢ bs || ds


Latex:


Latex:

1.  [T]  :  Type
2.  u  :  T
3.  v  :  T  List
4.  \mforall{}cs,bs,ds:T  List.    (v  @  bs  ||  cs  @  ds  {}\mRightarrow{}  bs  ||  ds  supposing  v  =  cs)
5.  u1  :  T
6.  v1  :  T  List
7.  \mforall{}bs,ds:T  List.    ([u  /  v]  @  bs  ||  v1  @  ds  {}\mRightarrow{}  bs  ||  ds  supposing  [u  /  v]  =  v1)
\mvdash{}  \mforall{}bs,ds:T  List.    ([u  /  v]  @  bs  ||  [u1  /  v1]  @  ds  {}\mRightarrow{}  bs  ||  ds  supposing  [u  /  v]  =  [u1  /  v1])


By


Latex:
Auto  \mcdot{}




Home Index