---

Step * 1 of Lemma rel_star_order


1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. WellFnd{i}(T;x,y.x R y)@i'
4. Trans(T;x,y.x (R^*) y)
5. x : T@i
6. y : T@i
7. x (R^*) y@i
8. y (R^*) x@i
⊢ x = y ∈ T
BY
{ (InstLemma `rel_plus_irreflexive` [⌜T⌝;⌜R⌝]⋅ THENA Auto) }

1
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. WellFnd{i}(T;x,y.x R y)@i'
4. Trans(T;x,y.x (R^*) y)
5. x : T@i
6. y : T@i
7. x (R^*) y@i
8. y (R^*) x@i
9. ∀x:T. (¬(x R+ x))
⊢ x = y ∈ T

---

Latex:

---

Latex:

1.  T  :  Type
2.  R  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  WellFnd\{i\}(T;x,y.x  R  y)@i'
4.  Trans(T;x,y.x  rel\_star(T;  R)  y)
5.  x  :  T@i
6.  y  :  T@i
7.  x  rel\_star(T;  R)  y@i
8.  y  rel\_star(T;  R)  x@i
\mvdash{}  x  =  y


By

---

Latex:
(InstLemma  `rel\_plus\_irreflexive`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index