Step
*
1
1
1
of Lemma
perm_igrp_wf
1. T : Type
⊢ ∀[x,y,z:Perm(T)]. (x O y O z = x O y O z ∈ Perm(T))
BY
{ MoveToConcl 1 }
1
∀T:Type. ∀[x,y,z:Perm(T)]. (x O y O z = x O y O z ∈ Perm(T))
Latex:
Latex:
1. T : Type
\mvdash{} \mforall{}[x,y,z:Perm(T)]. (x O y O z = x O y O z)
By
Latex:
MoveToConcl 1
Home
Index