Step
*
of Lemma
permr_upto_wf
∀T:Type. ∀R:T ⟶ T ⟶ ℙ. ∀as,bs:T List. (as ≡ bs upto x,y.R[x;y] ∈ ℙ)
BY
{ (Unfold `permr_upto` 0 THEN Auto') }
Latex:
Latex:
\mforall{}T:Type. \mforall{}R:T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}. \mforall{}as,bs:T List. (as \mequiv{} bs upto x,y.R[x;y] \mmember{} \mBbbP{})
By
Latex:
(Unfold `permr\_upto` 0 THEN Auto')
Home
Index