Step
*
of Lemma
permute_list_length
∀[T:Type]. ∀[L:T List]. ∀[f:Top]. (||(L o f)|| ~ ||L||)
BY
{ ((UnivCD THENA Auto) THEN (Unfold `permute_list` 0 THEN RWO "mklist_length" 0 THEN Auto)⋅) }
Latex:
Latex:
\mforall{}[T:Type]. \mforall{}[L:T List]. \mforall{}[f:Top]. (||(L o f)|| \msim{} ||L||)
By
Latex:
((UnivCD THENA Auto) THEN (Unfold `permute\_list` 0 THEN RWO "mklist\_length" 0 THEN Auto)\mcdot{})
Home
Index