Step
*
of Lemma
no_repeats-pairs-fpf
∀[A,B:Type]. ∀[eq1:EqDecider(A)]. ∀[eq2:EqDecider(B)]. ∀[L:(A × B) List]. no_repeats(A;fpf-domain(fpf(L)))
BY
{ ((InstLemma `pairs-fpf_property` []) THEN Repeat (ParallelLast) THEN Auto) }
Latex:
\mforall{}[A,B:Type]. \mforall{}[eq1:EqDecider(A)]. \mforall{}[eq2:EqDecider(B)]. \mforall{}[L:(A \mtimes{} B) List].
no\_repeats(A;fpf-domain(fpf(L)))
By
((InstLemma `pairs-fpf\_property` []) THEN Repeat (ParallelLast) THEN Auto)
Home
Index