Step
*
of Lemma
comb_for_grp_leq_wf
λg,a,b,z. (a ≤ b) ∈ g:GrpSig ⟶ a:|g| ⟶ b:|g| ⟶ (↓True) ⟶ ℙ
BY
{ ProveOpCombTyping `grp_leq_wf` }
Latex:
Latex:
\mlambda{}g,a,b,z. (a \mleq{} b) \mmember{} g:GrpSig {}\mrightarrow{} a:|g| {}\mrightarrow{} b:|g| {}\mrightarrow{} (\mdownarrow{}True) {}\mrightarrow{} \mBbbP{}
By
Latex:
ProveOpCombTyping `grp\_leq\_wf`
Home
Index