Step
*
of Lemma
rel_or-restriction
∀[T:Type]. ∀[P,Q:T ⟶ ℙ]. ∀[R:T ⟶ T ⟶ ℙ]. R|P ∨ R|Q => R|P ∨ Q
BY
{ (RepUR ``rel-restriction rel_or predicate_or rel_implies`` 0 THEN Auto THEN ProveProp THEN Auto) }
Latex:
Latex:
\mforall{}[T:Type]. \mforall{}[P,Q:T {}\mrightarrow{} \mBbbP{}]. \mforall{}[R:T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}]. R|P \mvee{} R|Q => R|P \mvee{} Q
By
Latex:
(RepUR ``rel-restriction rel\_or predicate\_or rel\_implies`` 0 THEN Auto THEN ProveProp THEN Auto)
Home
Index