---

Step * 1 of Lemma pairs-fpf_property


1. [A] : Type
2. [B] : Type
3. eq1 : EqDecider(A)
4. eq2 : EqDecider(B)
5. L : (A × B) List
⊢ no_repeats(A;fpf-domain(fpf(L)))
BY
{ xxx(Unfolds ``fpf-domain pairs-fpf`` 0
      THEN Reduce 0
      THEN (InstLemma `remove-repeats_property` [⌜A⌝; ⌜eq1⌝; ⌜map(λp.(fst(p));L)⌝])⋅
      THEN Auto)xxx }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  Type
3.  eq1  :  EqDecider(A)
4.  eq2  :  EqDecider(B)
5.  L  :  (A  \mtimes{}  B)  List
\mvdash{}  no\_repeats(A;fpf-domain(fpf(L)))


By

---

Latex:
xxx(Unfolds  ``fpf-domain  pairs-fpf``  0
        THEN  Reduce  0
        THEN  (InstLemma  `remove-repeats\_property`  [\mkleeneopen{}A\mkleeneclose{};  \mkleeneopen{}eq1\mkleeneclose{};  \mkleeneopen{}map(\mlambda{}p.(fst(p));L)\mkleeneclose{}])\mcdot{}
        THEN  Auto)xxx

---

Home Index