Step * of Lemma rel-rel-plus

[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀x,y:T.  ((x y)  (x R+ y))
BY
(Auto THEN Unfold `rel_plus` THEN Reduce 0) }

1
1. [T] Type
2. [R] T ⟶ T ⟶ ℙ
3. T@i
4. T@i
5. y@i
⊢ ∃n:ℕ+(x R^n y)


Latex:


Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    \mforall{}x,y:T.    ((x  R  y)  {}\mRightarrow{}  (x  R\msupplus{}  y))


By


Latex:
(Auto  THEN  Unfold  `rel\_plus`  0  THEN  Reduce  0)




Home Index