---

Step * 2 1 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
{ (((FLemma `permr_inversion` [9] THENM FLemma `permr_transitivity` [8; 10]) THENM FLemma `permr_transitivity` [12; 11])
   THEN Auto
   ) }

---

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:
(((FLemma  `permr\_inversion`  [9]  THENM  FLemma  `permr\_transitivity`  [8;  10])
  THENM  FLemma  `permr\_transitivity`  [12;  11]
  )
  THEN  Auto
  )

---

Home Index