---

{ [i:Id]. [a:Atom1].  uiff(i:Id||a;True) }

{ Proof }

---

Definitions occuring in Statement :  Id: Id,  uiff: uiff(P;Q),  uall: [x:A]. B[x],  true: True,  free-from-atom: x:T||a,  atom: Atom$n
Definitions :  uall: [x:A]. B[x],  Id: Id,  uiff: uiff(P;Q),  true: True,  member: t  T,  and: P  Q,  uimplies: b supposing a,  prop:
Lemmas :  free-from-atom_wf1,  true_wf

---

\mforall{}[i:Id].  \mforall{}[a:Atom1].    uiff(i:Id||a;True)


Date html generated: 2011_08_10-AM-07_43_29
Last ObjectModification: 2011_06_18-AM-08_09_59

Home Index