Step * 1 of Lemma permutation-nil-iff


1. Type
2. List
3. permutation(A;[];L)
⊢ [] ∈ (A List)
BY
((FLemma `permutation-length` [-1] THEN Auto) THEN DVar `L' THEN Auto') }


Latex:


Latex:

1.  A  :  Type
2.  L  :  A  List
3.  permutation(A;[];L)
\mvdash{}  L  =  []


By


Latex:
((FLemma  `permutation-length`  [-1]  THEN  Auto)  THEN  DVar  `L'  THEN  Auto')




Home Index