---

Step * 1 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` [8] THENM FLemma `permr_transitivity` [11; 10]) THENM FLemma `permr_transitivity` [12; 9])
   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`  [8]  THENM  FLemma  `permr\_transitivity`  [11;  10])
  THENM  FLemma  `permr\_transitivity`  [12;  9]
  )
  THEN  Auto
  )

---

Home Index