---

Step * of Lemma permr_transitivity

∀T:Type. ∀as,bs,cs:T List.  ((as ≡(T) bs) ⇒ (bs ≡(T) cs) ⇒ (as ≡(T) cs))
BY
{ ((UnivCD THENA Auto) THEN OnClauses [0; -1; -2] (Unfold `permr`)) }

1
1. T : Type
2. as : T List
3. bs : T List
4. cs : T List
5. (||as|| = ||bs|| ∈ ℤ) c∧ (∃p:Sym(||as||). ∀i:ℕ||as||. (as[p.f i] = bs[i] ∈ T))
6. (||bs|| = ||cs|| ∈ ℤ) c∧ (∃p:Sym(||bs||). ∀i:ℕ||bs||. (bs[p.f i] = cs[i] ∈ T))
⊢ (||as|| = ||cs|| ∈ ℤ) c∧ (∃p:Sym(||as||). ∀i:ℕ||as||. (as[p.f i] = cs[i] ∈ T))

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}as,bs,cs:T  List.    ((as  \mequiv{}(T)  bs)  {}\mRightarrow{}  (bs  \mequiv{}(T)  cs)  {}\mRightarrow{}  (as  \mequiv{}(T)  cs))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  OnClauses  [0;  -1;  -2]  (Unfold  `permr`))

---

Home Index