---

Step * 3 1 2 of Lemma free-dl_wf


1. X : Type@i'
2. as : X List List@i
3. bs : X List List@i
4. a1 : X List List@i
5. b1 : X List List@i
6. ∀x:X List. ((x ∈ bs) ⇒ (∃y:X List. ((y ∈ as) ∧ l_subset(X;y;x))))
7. ∀x:X List. ((x ∈ as) ⇒ (∃y:X List. ((y ∈ bs) ∧ l_subset(X;y;x))))
8. ∀x:X List. ((x ∈ b1) ⇒ (∃y:X List. ((y ∈ a1) ∧ l_subset(X;y;x))))
9. ∀x:X List. ((x ∈ a1) ⇒ (∃y:X List. ((y ∈ b1) ∧ l_subset(X;y;x))))
10. ∀x:X List
      ((∃u,v:X List. ((u ∈ b1) ∧ (v ∈ bs) ∧ (x = (u @ v) ∈ (X List))))
      ⇒ (∃y:X List. ((∃u,v:X List. ((u ∈ as) ∧ (v ∈ a1) ∧ (y = (u @ v) ∈ (X List)))) ∧ l_subset(X;y;x))))
11. x : X List@i
12. u : X List@i
13. v : X List@i
14. (u ∈ as)
15. (v ∈ a1)
16. x = (u @ v) ∈ (X List)
⊢ ∃y:X List. ((∃u,v:X List. ((u ∈ b1) ∧ (v ∈ bs) ∧ (y = (u @ v) ∈ (X List)))) ∧ l_subset(X;y;x))
BY
{ ((FHyp 7 [-3] THENA Auto) THEN (FHyp 9 [-3] THENA Auto) THEN ExRepD) }

1
1. X : Type@i'
2. as : X List List@i
3. bs : X List List@i
4. a1 : X List List@i
5. b1 : X List List@i
6. ∀x:X List. ((x ∈ bs) ⇒ (∃y:X List. ((y ∈ as) ∧ l_subset(X;y;x))))
7. ∀x:X List. ((x ∈ as) ⇒ (∃y:X List. ((y ∈ bs) ∧ l_subset(X;y;x))))
8. ∀x:X List. ((x ∈ b1) ⇒ (∃y:X List. ((y ∈ a1) ∧ l_subset(X;y;x))))
9. ∀x:X List. ((x ∈ a1) ⇒ (∃y:X List. ((y ∈ b1) ∧ l_subset(X;y;x))))
10. ∀x:X List
      ((∃u,v:X List. ((u ∈ b1) ∧ (v ∈ bs) ∧ (x = (u @ v) ∈ (X List))))
      ⇒ (∃y:X List. ((∃u,v:X List. ((u ∈ as) ∧ (v ∈ a1) ∧ (y = (u @ v) ∈ (X List)))) ∧ l_subset(X;y;x))))
11. x : X List@i
12. u : X List@i
13. v : X List@i
14. (u ∈ as)
15. (v ∈ a1)
16. x = (u @ v) ∈ (X List)
17. y1 : X List
18. (y1 ∈ bs)
19. l_subset(X;y1;u)
20. y : X List
21. (y ∈ b1)
22. l_subset(X;y;v)
⊢ ∃y:X List. ((∃u,v:X List. ((u ∈ b1) ∧ (v ∈ bs) ∧ (y = (u @ v) ∈ (X List)))) ∧ l_subset(X;y;x))

---

Latex:

---

Latex:

1.  X  :  Type@i'
2.  as  :  X  List  List@i
3.  bs  :  X  List  List@i
4.  a1  :  X  List  List@i
5.  b1  :  X  List  List@i
6.  \mforall{}x:X  List.  ((x  \mmember{}  bs)  {}\mRightarrow{}  (\mexists{}y:X  List.  ((y  \mmember{}  as)  \mwedge{}  l\_subset(X;y;x))))
7.  \mforall{}x:X  List.  ((x  \mmember{}  as)  {}\mRightarrow{}  (\mexists{}y:X  List.  ((y  \mmember{}  bs)  \mwedge{}  l\_subset(X;y;x))))
8.  \mforall{}x:X  List.  ((x  \mmember{}  b1)  {}\mRightarrow{}  (\mexists{}y:X  List.  ((y  \mmember{}  a1)  \mwedge{}  l\_subset(X;y;x))))
9.  \mforall{}x:X  List.  ((x  \mmember{}  a1)  {}\mRightarrow{}  (\mexists{}y:X  List.  ((y  \mmember{}  b1)  \mwedge{}  l\_subset(X;y;x))))
10.  \mforall{}x:X  List
            ((\mexists{}u,v:X  List.  ((u  \mmember{}  b1)  \mwedge{}  (v  \mmember{}  bs)  \mwedge{}  (x  =  (u  @  v))))
            {}\mRightarrow{}  (\mexists{}y:X  List.  ((\mexists{}u,v:X  List.  ((u  \mmember{}  as)  \mwedge{}  (v  \mmember{}  a1)  \mwedge{}  (y  =  (u  @  v))))  \mwedge{}  l\_subset(X;y;x))))
11.  x  :  X  List@i
12.  u  :  X  List@i
13.  v  :  X  List@i
14.  (u  \mmember{}  as)
15.  (v  \mmember{}  a1)
16.  x  =  (u  @  v)
\mvdash{}  \mexists{}y:X  List.  ((\mexists{}u,v:X  List.  ((u  \mmember{}  b1)  \mwedge{}  (v  \mmember{}  bs)  \mwedge{}  (y  =  (u  @  v))))  \mwedge{}  l\_subset(X;y;x))


By

---

Latex:
((FHyp  7  [-3]  THENA  Auto)  THEN  (FHyp  9  [-3]  THENA  Auto)  THEN  ExRepD)

---

Home Index