---

Step * 1 of Lemma before_trans


1. a : LOSet@i'
2. u : |a|@i
3. v : |a|@i
4. u1 : |a|
5. v1 : |a| List
6. v <a u@i
7. u1 <a v@i
⊢ u1 <a u
BY
{ ((FLemma `qoset_lt_trans` [6;7]) THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  LOSet@i'
2.  u  :  |a|@i
3.  v  :  |a|@i
4.  u1  :  |a|
5.  v1  :  |a|  List
6.  v  <a  u@i
7.  u1  <a  v@i
\mvdash{}  u1  <a  u


By

---

Latex:
((FLemma  `qoset\_lt\_trans`  [6;7])  THEN  Auto)

---

Home Index