---

{ [a,A:Type].  (inning_vote()  A  a  a) }

{ Proof }

---

Definitions occuring in Statement :  inning_vote: inning_vote(),  uall: [x:A]. B[x],  member: t  T,  function: x:A  B[x],  product: x:A  B[x],  universe: Type
Definitions :  uall: [x:A]. B[x],  member: t  T,  inning_vote: inning_vote(),  so_lambda: x.t[x],  so_apply: x[s]
Lemmas :  pi2_wf

---

\mforall{}[a,A:Type].    (inning\_vote()  \mmember{}  A  \mtimes{}  a  {}\mrightarrow{}  a)


Date html generated: 2011_08_17-PM-06_33_07
Last ObjectModification: 2011_06_18-AM-11_56_24

Home Index