---

Step * 2 of Lemma permr_functionality_wrt_permr


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
BY
{ (RWH (RevHypC 7) 10 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

---

Latex:

---

Latex:

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'
8.  as  \mequiv{}(T)  as'
9.  bs  \mequiv{}(T)  bs'
10.  as'  \mequiv{}(T')  bs'
\mvdash{}  as  \mequiv{}(T)  bs


By

---

Latex:
(RWH  (RevHypC  7)  10  THENA  Auto)

---

Home Index