---

Step * 1 2 2 of Lemma rel_le_sp_refl_cl


1. [T] : Type
2. [r] : T ⟶ T ⟶ ℙ
3. ∀[a:T]. (¬(r a a))
4. ∀x,y:T.  (¬((r x y) ∧ (r y x)))
5. x : T@i
6. y : T@i
7. r x y@i
8. r y x@i
⊢ False
BY
{ % need better matching for chaining % 
((InstHyp [x;y] 4 THENM D (-1)) THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [r]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}[a:T].  (\mneg{}(r  a  a))
4.  \mforall{}x,y:T.    (\mneg{}((r  x  y)  \mwedge{}  (r  y  x)))
5.  x  :  T@i
6.  y  :  T@i
7.  r  x  y@i
8.  r  y  x@i
\mvdash{}  False


By

---

Latex:
\%  need  better  matching  for  chaining  \% 
((InstHyp  [x;y]  4  THENM  D  (-1))  THEN  Auto)

---

Home Index