---

Step * of Lemma permr_upto_functionality_wrt_permr_upto

∀T:Type. ∀R:T ⟶ T ⟶ ℙ.
  (EquivRel(T;x,y.R[x;y])
  ⇒ (∀as,as',bs,bs':T List.
        (as ≡ bs upto x,y.R[x;y] 
        ⇒ as' ≡ bs' upto x,y.R[x;y] 
        ⇒ (as ≡ as' upto x,y.R[x;y]  ⇐⇒ bs ≡ bs' upto x,y.R[x;y] ))))
BY
{ (RepeatMFor 3 (D 0) THENA Auto) }

1
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. EquivRel(T;x,y.R[x;y])
⊢ ∀as,as',bs,bs':T List.
    (as ≡ bs upto x,y.R[x;y] 
    ⇒ as' ≡ bs' upto x,y.R[x;y] 
    ⇒ (as ≡ as' upto x,y.R[x;y]  ⇐⇒ bs ≡ bs' upto x,y.R[x;y] ))

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.
    (EquivRel(T;x,y.R[x;y])
    {}\mRightarrow{}  (\mforall{}as,as',bs,bs':T  List.
                (as  \mequiv{}  bs  upto  x,y.R[x;y] 
                {}\mRightarrow{}  as'  \mequiv{}  bs'  upto  x,y.R[x;y] 
                {}\mRightarrow{}  (as  \mequiv{}  as'  upto  x,y.R[x;y]    \mLeftarrow{}{}\mRightarrow{}  bs  \mequiv{}  bs'  upto  x,y.R[x;y]  ))))


By

---

Latex:
(RepeatMFor  3  (D  0)  THENA  Auto)

---

Home Index