---

Step * of Lemma mk_igrp_wf

∀[T:Type]. ∀[op:T ⟶ T ⟶ T]. ∀[id:T]. ∀[inv:T ⟶ T].
  (mk_igrp(T;op;id;inv) ∈ IGroup) supposing (Inverse(T;op;id;inv) and Ident(T;op;id) and Assoc(T;op))
BY
{ ((Unfold `mk_igrp` 0 THEN UnivCD) THENA Auto) }

1
1. T : Type
2. op : T ⟶ T ⟶ T
3. id : T
4. inv : T ⟶ T
5. Assoc(T;op)
6. Ident(T;op;id)
7. Inverse(T;op;id;inv)
⊢ <T, λx,y. tt, λx,y. tt, op, id, inv> ∈ IGroup

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[op:T  {}\mrightarrow{}  T  {}\mrightarrow{}  T].  \mforall{}[id:T].  \mforall{}[inv:T  {}\mrightarrow{}  T].
    (mk\_igrp(T;op;id;inv)  \mmember{}  IGroup)  supposing 
          (Inverse(T;op;id;inv)  and 
          Ident(T;op;id)  and 
          Assoc(T;op))


By

---

Latex:
((Unfold  `mk\_igrp`  0  THEN  UnivCD)  THENA  Auto)

---

Home Index