---

Step * of Lemma permutation-iff-count1

∀[T:Type]
  ∀eq:T ⟶ T ⟶ 𝔹
    ((∀x,y:T.  (↑(eq x y) ⇐⇒ x = y ∈ T))
    ⇒ (∀a1,b1:T List.  (∀x:T. (||filter(eq x;a1)|| = ||filter(eq x;b1)|| ∈ ℤ) ⇐⇒ permutation(T;a1;b1))))
BY
{ Assert ⌜∀[T:Type]
            ∀eq:T ⟶ T ⟶ 𝔹
              ((∀x,y:T.  (↑(eq x y) ⇐⇒ x = y ∈ T))
              ⇒ (∀a1,b1:T List.  ((∀x:T. (||filter(eq x;a1)|| = ||filter(eq x;b1)|| ∈ ℤ)) ⇒ permutation(T;a1;b1))))⌝
⋅ }

1
.....assertion..... 
∀[T:Type]
  ∀eq:T ⟶ T ⟶ 𝔹
    ((∀x,y:T.  (↑(eq x y) ⇐⇒ x = y ∈ T))
    ⇒ (∀a1,b1:T List.  ((∀x:T. (||filter(eq x;a1)|| = ||filter(eq x;b1)|| ∈ ℤ)) ⇒ permutation(T;a1;b1))))

2
1. ∀[T:Type]
     ∀eq:T ⟶ T ⟶ 𝔹
       ((∀x,y:T.  (↑(eq x y) ⇐⇒ x = y ∈ T))
       ⇒ (∀a1,b1:T List.  ((∀x:T. (||filter(eq x;a1)|| = ||filter(eq x;b1)|| ∈ ℤ)) ⇒ permutation(T;a1;b1))))
⊢ ∀[T:Type]
    ∀eq:T ⟶ T ⟶ 𝔹
      ((∀x,y:T.  (↑(eq x y) ⇐⇒ x = y ∈ T))
      ⇒ (∀a1,b1:T List.  (∀x:T. (||filter(eq x;a1)|| = ||filter(eq x;b1)|| ∈ ℤ) ⇐⇒ permutation(T;a1;b1))))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}eq:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}
        ((\mforall{}x,y:T.    (\muparrow{}(eq  x  y)  \mLeftarrow{}{}\mRightarrow{}  x  =  y))
        {}\mRightarrow{}  (\mforall{}a1,b1:T  List.
                    (\mforall{}x:T.  (||filter(eq  x;a1)||  =  ||filter(eq  x;b1)||)  \mLeftarrow{}{}\mRightarrow{}  permutation(T;a1;b1))))


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}[T:Type]
                    \mforall{}eq:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}
                        ((\mforall{}x,y:T.    (\muparrow{}(eq  x  y)  \mLeftarrow{}{}\mRightarrow{}  x  =  y))
                        {}\mRightarrow{}  (\mforall{}a1,b1:T  List.
                                    ((\mforall{}x:T.  (||filter(eq  x;a1)||  =  ||filter(eq  x;b1)||))  {}\mRightarrow{}  permutation(T;a1;b1))))\mkleeneclose{}\mcdot{}

---

Home Index