---

Step * of Lemma permr_functionality_wrt_permr

∀T,T':Type. ∀as:T List. ∀as':T' List. ∀bs:T List. ∀bs':T' List.
  ((T = T' ∈ Type) ⇒ (as ≡(T) as') ⇒ (bs ≡(T) bs') ⇒ (as ≡(T) bs ⇐⇒ as' ≡(T') bs'))
BY
{ (GenUnivCD THENA Auto) }

1
1. T : Type
2. T' : Type
3. as : T List
4. as' : T' List
5. bs : T List
6. bs' : T' List
7. T = T' ∈ Type
8. as ≡(T) as'
9. bs ≡(T) bs'
10. as ≡(T) bs
⊢ as' ≡(T') bs'

2
1. T : Type
2. T' : Type
3. as : T List
4. as' : T' List
5. bs : T List
6. bs' : T' List
7. T = T' ∈ Type
8. as ≡(T) as'
9. bs ≡(T) bs'
10. as' ≡(T') bs'
⊢ as ≡(T) bs

---

Latex:

---

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


By

---

Latex:
(GenUnivCD  THENA  Auto)

---

Home Index