Step
*
of Lemma
comb_for_perm_sig_wf
λT,z. perm_sig(T) ∈ T:Type ⟶ (↓True) ⟶ Type
BY
{ (ProveOpCombinatorTyping Auto) `perm_sig_wf` }
Latex:
Latex:
\mlambda{}T,z.  perm\_sig(T)  \mmember{}  T:Type  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  Type
By
Latex:
(ProveOpCombinatorTyping  Auto)  `perm\_sig\_wf`
Home
Index