Step * of Lemma rel-plus-rel-immediate

[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  R!+ => R+
BY
(RepUR ``rel_implies rel_plus rel-immediate infix_ap`` THEN Auto THEN ParallelLast) }

1
1. [T] Type
2. [R] T ⟶ T ⟶ ℙ
3. T
4. T
5. : ℕ+
6. λx,y. ((R y) ∧ (∀z:T. ((R z) ∧ (R y)))))^n y
⊢ R^n y


Latex:


Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    R!\msupplus{}  =>  R\msupplus{}


By


Latex:
(RepUR  ``rel\_implies  rel\_plus  rel-immediate  infix\_ap``  0  THEN  Auto  THEN  ParallelLast)




Home Index