---

Step * 1 of Lemma fseg_transitivity


1. [T] : Type
2. l1 : T List
3. l2 : T List
4. l3 : T List
5. L1 : T List
6. l2 = (L1 @ l1) ∈ (T List)
7. L : T List
8. l3 = (L @ l2) ∈ (T List)
⊢ ∃L@0:T List. ((L @ L1 @ l1) = (L@0 @ l1) ∈ (T List))
BY
{ (InstConcl [L @ L1]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  l1  :  T  List
3.  l2  :  T  List
4.  l3  :  T  List
5.  L1  :  T  List
6.  l2  =  (L1  @  l1)
7.  L  :  T  List
8.  l3  =  (L  @  l2)
\mvdash{}  \mexists{}L@0:T  List.  ((L  @  L1  @  l1)  =  (L@0  @  l1))


By

---

Latex:
(InstConcl  [L  @  L1]\mcdot{}  THEN  Auto)

---

Home Index