---

Step * of Lemma tuple-equiv_wf

∀[L:(X:Type × (X ⟶ X ⟶ ℙ)) List]
  (tuple-equiv(L) ∈ tuple-type(map(λp.(fst(p));L)) ⟶ tuple-type(map(λp.(fst(p));L)) ⟶ ℙ)
BY
{ (ProveWfLemma THEN (DoSubsume THEN Auto) THEN RWO "select-map" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[L:(X:Type  \mtimes{}  (X  {}\mrightarrow{}  X  {}\mrightarrow{}  \mBbbP{}))  List]
    (tuple-equiv(L)  \mmember{}  tuple-type(map(\mlambda{}p.(fst(p));L))  {}\mrightarrow{}  tuple-type(map(\mlambda{}p.(fst(p));L))  {}\mrightarrow{}  \mBbbP{})


By

---

Latex:
(ProveWfLemma  THEN  (DoSubsume  THEN  Auto)  THEN  RWO  "select-map"  0  THEN  Auto)

---

Home Index