---

Step * 3 1 1 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
6. a : A
⊢ no_repeats(B;reduce(λp,l. if eqof(eq1) (fst(p)) a then insert(snd(p);l) else l fi ;[];L))
BY
{ xxx(Unfold `eqof` 0
      THEN (ListInd (-2))
      THEN Reduce 0
      THEN Try ((BLemma `no_repeats_nil` THEN Auto))
      THEN Try ((SplitOnConclITE THEN Auto THEN BLemma `no_repeats-insert` 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
6.  a  :  A
\mvdash{}  no\_repeats(B;reduce(\mlambda{}p,l.  if  eqof(eq1)  (fst(p))  a  then  insert(snd(p);l)  else  l  fi  ;[];L))


By

---

Latex:
xxx(Unfold  `eqof`  0
        THEN  (ListInd  (-2))
        THEN  Reduce  0
        THEN  Try  ((BLemma  `no\_repeats\_nil`  THEN  Auto))
        THEN  Try  ((SplitOnConclITE  THEN  Auto  THEN  BLemma  `no\_repeats-insert`  THEN  Auto)))xxx

---

Home Index